Skip to main navigation Skip to search Skip to main content

Hoare Logic for Disjunctive Information Flow

  • Hanne Riis Nielson
  • , Flemming Nielson
  • , Ximeng Li

Research output: Chapter in Book/Report/Conference proceedingBook chapterResearchpeer-review

Abstract

Information flow control extends access control by not only regulating who is allowed to access what data but also the subsequent use of the data accessed. Applications within communication networks require such information flow control to depend on the actual data. For a concurrent language with synchronous communication and separate data domains we develop a Hoare logic for enforcing disjunctive information flow policies. We establish the soundness of the Hoare logic with respect to an operational semantics and illustrate the development on a running example.
Original languageEnglish
Title of host publicationProgramming Languages with Applications to Biology and Security : Essays Dedicated to Pierpaolo Degano on the Occasion of His 65th Birthday
EditorsChiara Bodei, Gian-Luigi Ferrari, Corrado Priami
PublisherSpringer
Publication date2015
Pages47-65
ISBN (Print)978-3-319-25526-2
ISBN (Electronic)978-3-319-25527-9
DOIs
Publication statusPublished - 2015
SeriesLecture Notes in Computer Science
Volume9465
ISSN0302-9743

Fingerprint

Dive into the research topics of 'Hoare Logic for Disjunctive Information Flow'. Together they form a unique fingerprint.

Cite this