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 ...

• Type: Conference
• Year: 2010
• Where: ESOP
• Authors: Torben Amtoft, John Hatcliff and Edwin Rodríguez
• Keywords: ESOP 2010, Information Flow Annotations, Information Flow Policies, Programming Languages, SPARK Information Flow