Atomistic Galois insertions for flow sensitive integrity

Publication: Research - peer-reviewJournal article – Annual report year: 2017

DOI

View graph of relations

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.
Original languageEnglish
JournalComputer Languages, Systems and Structures
Volume50
Pages (from-to)82-107
ISSN1477-8424
DOIs
StatePublished - 2017
CitationsWeb of Science® Times Cited: No match on DOI

    Keywords

  • Computer Theory (Includes Formal Logic, Automata Theory, Switching Theory and Programming Theory), Computer Applications, Accidents and Accident Prevention, Abstract interpretation, Information flow, Security policy, Security systems, Verification, Abstract interpretations, Concurrent languages, Flow sensitive, Information flows, Program Verification, Synchronous communications, User assistance, Static analysis
Download as:
Download as PDF
Select render style:
APAAuthorCBE/CSEHarvardMLAStandardVancouverShortLong
PDF
Download as HTML
Select render style:
APAAuthorCBE/CSEHarvardMLAStandardVancouverShortLong
HTML
Download as Word
Select render style:
APAAuthorCBE/CSEHarvardMLAStandardVancouverShortLong
Word

ID: 134063288