Atomistic Galois insertions for flow sensitive integrity. (December 2017)

• Record Type: Journal Article
• Authors: Nielson, Flemming; Riis Nielson, Hanne
• Is Part Of: Computer languages, systems & structures. Volume 50(2017)
• Page Start: 82
• Page End: 107
• Publication Date: 2017-12
• Subjects: Abstract interpretation -- Security policy -- Information flow; Programming languages (Electronic computers) -- Periodicals; Computer networks -- Periodicals; Computer architecture -- Periodicals; Computer systems -- Periodicals; Langage de programmation; Réseau d'ordinateurs; Architecture d'ordinateur; Périodique électronique (Descripteur de forme); Ressource Internet (Descripteur de forme); 005.13
• DOI: 10.1016/j.cl.2017.06.004
• Languages: English
• ISSNs: 1477-8424

Abstract

Highlights: We develop the theory of atomistic Galois insertions to link abstract security policies with the results of static analyses. We use this to impose a content dependent information flow policy on a concurrent language with polyadic synchronous communication and local storage. The running example illustrates the approach on a multiplexer–demultiplexer scenario originating from avionics. We establish semantic soundness through an instrumented semantics dealing with explicit and implicit information flow. Abstract: Several program verification techniques assist in showing that software adheres to the required security policies. Such policies may be sensitive to the flow of execution and the verification may be supported by combinations of type systems and Hoare logics. However, this requires user assistance and to obtain full automation we shall explore the over-approximating nature of static analysis. We demonstrate that the use of atomistic Galois insertions constitutes a stable framework in which to obtain sound and fully automatic enforcement of flow sensitive integrity. The framework is illustrated on a concurrent language with local storage and polyadic synchronous communication.