Abstract: This talk studies the problem of resource availability in the context of mobile code for embedded systems such as smart cards. It presents an architecture dedicated to controlling the usage of a single resource in a multi-process operating system. Its specificity lies in its ability to improve the task scheduling in order to spare resources. Our architecture comprises two parts. The first statically computes the resource needs using a dedicated lattice. The second guarantees at runtime that there will always be enough resources for every application to terminate, thanks to an efficient deadlock-avoidance algorithm. The example studied here is an implementation on a JVM (Java Virtual Machine) for smart cards, dealing with a realistic subset of the Java bytecode. Details of this work have been presented in APLAS`03.
Abstract (updated version): We give a brief overview over our applied research on formal security modeling and verification at Siemens Corporate Technology. We have developed a formalism called Interacting State Machines (ISMs) tailored for analyzing reactive state-oriented systems. It is integrated in the interactive theorem prover Isabelle/HOL and uses the CASE tool AutoFocus as a graphical front end. We have used this framework for (higher-level) evaluation of smart card processor hardware SLE 66 and SLE 88 by Infineon, analysis of a medical data base software by Siemens MED, and currently for modeling a document management system by Boeing. We have extended ISMs for dealing with dynamic and ambient-like communication patterns and applied them in the German BMWA project MAP. We model, verify, and improve industrial-scale crypto protocols with the help of automatic tools like the infinite-state model checker OFMC, e.g. in the EU project AVISPA. Recently, we have introduced noninfluence and nonleakage, some variants of noninterference well suited for describing and proving secure information flow in state-oriented systems.
Abstract: Software test engineers at Microsoft test software by observing its external behavior, a process that is usually called black-box testing. Despite its prominent role in commercial software development, black-box testing's many hard problems have not received enough attention in the research community. During the recent years this situation has changed though, Microsoft Research has developed powerful new techniques for black-box testing of .NET components. These techniques are exposed through a new specification language called Spec\# together with a suite of advanced testing tools. Spec\# is an extension of C\# with contracts, in form of pre- and post-conditions, and language features suitable for high-level behavioral models. Specifications written in Spec\# can be exploited for systematic model-based test-case generation that allow testers to go beyond manual test-cases, robustness testing and syntactic code-coverage, to semantic model-based state-space exploration techniques. Such developments are not a mere trend but a necessary development driven by increasing demands on software quality.