Journal article
Atomistic Galois insertions for flow sensitive integrity
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.
Language: | English |
---|---|
Year: | 2017 |
Pages: | 82-107 |
ISSN: | 18736866 and 14778424 |
Types: | Journal article |
DOI: | 10.1016/j.cl.2017.06.004 |
ORCIDs: | Nielson, Flemming and Nielson, Hanne Riis |
Abstract interpretation Abstract interpretations Accidents and Accident Prevention Computer Applications Computer Theory (Includes Formal Logic, Automata Theory, Switching Theory and Programming Theory) Concurrent languages Flow sensitive Information flow Information flows Program Verification Security policy Security systems Static analysis Synchronous communications User assistance Verification