From coupling relations to mated invariants for checking information flow

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

42 Scopus citations

Abstract

This paper investigates a technique for using automated program verifiers to check conformance with information flow policy, in particular for programs acting on shared, dynamically allocated mutable heap objects. The technique encompasses rich policies with forms of declassification and supports modular, invariant-based verification of object-oriented programs. The technique is based on the known idea of self-composition, whereby noninterference for a command is reduced to an ordinary partial correctness property of the command sequentially composed with a renamed copy of itself. The first contribution is to extend this technique to encompass heap objects, which is difficult because textual renaming is inapplicable. The second contribution is a systematic means to validate transformations on self-composed programs. Certain transformations are needed for effective use of existing automated program verifiers and they exploit conservative flow inference, e.g., from security type inference. Experiments with the technique using ESC/Java2 and Spec# verifiers are reported.

Original languageEnglish
Title of host publicationComputer Security - ESORICS 2006 - 11th European Symposium on Research in Computer Security, Proceedings
Pages279-296
Number of pages18
DOIs
StatePublished - 2006
Event11th European Symposium on Research in Computer Security, ESORICS 2006 - Hamburg, Germany
Duration: 18 Sep 200620 Sep 2006

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume4189 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference11th European Symposium on Research in Computer Security, ESORICS 2006
Country/TerritoryGermany
CityHamburg
Period18/09/0620/09/06

Fingerprint

Dive into the research topics of 'From coupling relations to mated invariants for checking information flow'. Together they form a unique fingerprint.

Cite this