Sciweavers

Share
ESOP
2010
Springer

Precise and Automated Contract-based Reasoning for Verification and Certification of Information Flow Properties of Programs wit

9 years 4 months ago
Precise and Automated Contract-based Reasoning for Verification and Certification of Information Flow Properties of Programs wit
Abstract. Embedded information assurance applications that are critical to national and international infrastructures, must often adhere to certification regimes that require information flow properties to be specified and verified. SPARK, a subset of Ada for engineering safety critical systems, is being used to develop multiple certified information assurance systems. While SPARK provides information flow annotations and associated automated checking mechanisms, industrial experience has revealed that these annotations are not precise enough to specify many desired information flow policies. One key problem is that arrays are treated as indivisible entities ? flows that involve only particular locations of have to be abstracted into flows on the whole array. This has substantial practical impact since SPARK does not allow dynamic allocation of memory, and hence makes heavy use of arrays to implement complex data structures. In this paper, we present a Hoare logic for information flow ...
Torben Amtoft, John Hatcliff and Edwin Rodríguez
Added 02 Mar 2010
Updated 02 Mar 2010
Type Conference
Year 2010
Where ESOP
Authors Torben Amtoft, John Hatcliff and Edwin Rodríguez
Comments (0)
books