Atomistic Galois insertions for flow sensitive integrity

Flemming Nielson; Hanne Riis Nielson

doi:10.1016/j.cl.2017.06.004

Atomistic Galois insertions for flow sensitive integrity

Research output: Contribution to journal › Journal article › Research › peer-review

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.

Original language	English
Journal	Computer Languages, Systems and Structures
Volume	50
Pages (from-to)	82-107
ISSN	1477-8424
DOIs	https://doi.org/10.1016/j.cl.2017.06.004
Publication status	Published - 2017

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

Access to Document

10.1016/j.cl.2017.06.004

Fingerprint Dive into the research topics of 'Atomistic Galois insertions for flow sensitive integrity'. Together they form a unique fingerprint.

Cite this

@article{ae4370cb3d734763849ce157c559c95c,

title = "Atomistic Galois insertions for flow sensitive integrity",

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

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",

author = "Flemming Nielson and Nielson, {Hanne Riis}",

year = "2017",

doi = "10.1016/j.cl.2017.06.004",

language = "English",

volume = "50",

pages = "82--107",

journal = "Computer Languages, Systems and Structures",

issn = "1477-8424",

publisher = "Pergamon Press",

}

TY - JOUR

T1 - Atomistic Galois insertions for flow sensitive integrity

AU - Nielson, Flemming

AU - Nielson, Hanne Riis

PY - 2017

Y1 - 2017

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

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

KW - Computer Theory (Includes Formal Logic, Automata Theory, Switching Theory and Programming Theory)

KW - Computer Applications

KW - Accidents and Accident Prevention

KW - Abstract interpretation

KW - Information flow

KW - Security policy

KW - Security systems

KW - Verification

KW - Abstract interpretations

KW - Concurrent languages

KW - Flow sensitive

KW - Information flows

KW - Program Verification

KW - Synchronous communications

KW - User assistance

KW - Static analysis

U2 - 10.1016/j.cl.2017.06.004

DO - 10.1016/j.cl.2017.06.004

M3 - Journal article

VL - 50

SP - 82

EP - 107

JO - Computer Languages, Systems and Structures

JF - Computer Languages, Systems and Structures

SN - 1477-8424

ER -