Assume but Verify: Deductive Verification of Leaked Information in Concurrent Applications

Toby Murray, Mukesh Tiwari, Gidon Ernst, David A. Naumann

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

2 Scopus citations

Abstract

We consider the problem of specifying and proving the security of non-trivial, concurrent programs that intentionally leak information. We present a method that decomposes the problem into (a) proving that the program only leaks information it has declassified via assume annotations already widely used in deductive program verification; and (b) auditing the declassifications against a declarative security policy. We show how condition (a) can be enforced by an extension of the existing program logic SecCSL, and how (b) can be checked by proving a set of simple entailments. Part of the challenge is to define respective semantic soundness criteria and to formally connect these to the logic rules and policy audit. We support our methodology in an auto-active program verifier, which we apply to verify the implementations of various case study programs against a range of declassification policies.

Original languageEnglish
Title of host publicationCCS 2023 - Proceedings of the 2023 ACM SIGSAC Conference on Computer and Communications Security
Pages1746-1760
Number of pages15
ISBN (Electronic)9798400700507
DOIs
StatePublished - 15 Nov 2023
Event30th ACM SIGSAC Conference on Computer and Communications Security, CCS 2023 - Copenhagen, Denmark
Duration: 26 Nov 202330 Nov 2023

Publication series

NameCCS 2023 - Proceedings of the 2023 ACM SIGSAC Conference on Computer and Communications Security

Conference

Conference30th ACM SIGSAC Conference on Computer and Communications Security, CCS 2023
Country/TerritoryDenmark
CityCopenhagen
Period26/11/2330/11/23

Keywords

  • declassification
  • information flow security
  • program verification

Fingerprint

Dive into the research topics of 'Assume but Verify: Deductive Verification of Leaked Information in Concurrent Applications'. Together they form a unique fingerprint.

Cite this