Egon Börger, University of Pisa
Using Abstract State Machines for Design and Analysis of Software-Based Systems
Abstract: In this talk I review the notion of Abstract State Machine (ASM) and
present some of the highlights of its applications for design and
analysis of software-based systems. In particular I will discuss
methods of composition and of refinement of ASMs which are crucial for
building verifiable systems out of verified components.
David von Oheimb, Siemens
A Formal Security Model of the Infineon SLE 88 Smart Card Memory Management
Abstract: The Infineon SLE 88 is a smart card processor that offers strong
protection mechanisms. One of them is a memory management system,
typically used for sandboxing application programs dynamically loaded
on the chip. High-level (EAL5+) evaluation of the chip requires
a formal security model.
We formally model the memory management system as an Interacting State
Machine and prove, using Isabelle/HOL, that the associated security
requirements are met. We demonstrate that our approach enables an
adequate level of abstraction, which results in an efficient analysis,
and points out potential pitfalls like non-injective address translation.
Dominique Borrione, University Joseph Fourier (Grenoble)
Combining Several Paradigms for Circuit Validation and Verfication
Abstract: The formal specification of circuit components is routinely performed at
the register transfer level (RTL), which serves as input to automatic
synthesis and property verification software. But when the specification is
more abstract, both the initial validation and the first implementation
verification involve extensive simulation of numeric values, or extensive
expert human time to apply mechanized, but non-automatic, transformations
and theorem proving techniques. Unfortunately, the RTL input to the
synthesis software rarely has been proven compliant to the higher-level
specification. To solve this difficulty, we formalize the simulation
semantics of standard design languages, and look for synergies between
numeric and symbolic techniques.
The first step is the functional specification of the data path. It is
formalized in Lisp, and can be executed on test benches, to check that the
returned result is as expected. A more formal validation is obtained by
proving the mathematical properties of the algorithm, using the ACL2
theorem prover. The verification of the early design steps of the data path
combines simulation of test cases, symbolic simulation and theorem proving,
as complementary techniques. A cycle-based simulator for a synthesizable
VHDL subset has been implemented over the Mathematica symbolic computation
engine, and algebraic terms are simplified on the fly. We simulate the
model symbolically for one clock cycle, in effect corresponding to several
VHDL simulation cycles, to extract the transition function for each output
and state variable. The proofs are then conducted on this model, translated
to Lisp, with the ACL2 theorem prover.
The verification of the control part aims at establishing the fulfillment
of logic and temporal properties, and the correct synchronization of
concurrent sub-parts. A drastic reduction of the data path is needed to
make model checking at all possible. Decomposition strategies help reduce
the size of the model. For designs that are characterized by a set of
mutually exclusive operating modes, a combination of symbolic simulation
and symbolic model checking improves the verification efficiency.
Alessandro Coglio, Kestrel Institute
Toward Synthesis of Provably Correct Java Card Applets and Platform
Abstract: This talk overviews an ongoing project aimed at developing (1) an automatic generator of Java Card applets from high-level specifications and (2) a specification of the Java Card platform along with refinements to implementations. Both developments are based on Kestrel's Specware, a system for the formal specification and refinement of software.
The applet generator translates a specification written in a domain-specific language called "SmartSlang" into the logical language of Specware, re-expresses the translated specification in terms of Java Card concepts via a series of refinement steps using Specware's machinery, and generates Java Card code from the refined specification. The Java Card concepts used for refinement and code generation are captured as a shallow embedding of the Java Card language and API in the logic of Specware. Since proofs are associated to refinement steps, the applet generator produces a machine-processable proof tree along with the code, enabling the correctness of the generated code (with respect to the specification) to be checked independently from the applet generator, via a smaller and simpler applet checker to be also developed in this project.
The specification of the Java Card platform, which includes the CAP file format, the bytecode interpreter, the API, and the Java Card-specific security mechanisms like the applet firewall, is written in Specware. Using Specware's refinement machinery, the specification is (manually) refined to (i) code to be run on desktop computers for simulation and (ii) code to be run on actual smart cards for deployment. Discharging the proof obligations generated by Specware during refinement guarantees that both implementations are correct with respect to the specification.