A security logic for abstract state machines. We extend the logic for Abstract State Machines by a read predicate that allows to make precise statements about the accesses of locations of an ASM. The logic can be used to prove security properties of ASMs like that the machine does not read locations containing critical information or that all accesses of the machine are in a well-defined region of the abstract memory. The new read predicate is also useful for proving refinements of parallel ASMs to sequential C-like programs. The logic is complete for hierarchical ASMs and still sound for turbo ASMs. It is integrated in the ASMKeY theorem prover.
Keywords for this software
References in zbMATH (referenced in 6 articles )
Showing results 1 to 6 of 6.
- Ahrendt, Wolfgang; Dylla, Maximilian: A system for compositional verification of asynchronous objects (2012)
- Ahrendt, Wolfgang; Beckert, Bernhard; Hähnle, Reiner; Schmitt, Peter H.: KeY: A formal method for object-oriented systems (2007)
- Börger, Egon: Construction and analysis of ground models and their refinements as a foundation for validating computer-based systems (2007)
- Nanchen, Stanislas; Stärk, Robert F.: A logic for secure memory access of abstract state machines (2005)
- Stärk, Robert F.: Formal specification and verification of the C(#) thread model (2005)
- Nanchen, Stanislas; Stärk, Robert F.: A security logic for abstract state machines (2004)