No Cover Image

Conference Paper/Proceeding/Abstract 25 views

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

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

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

Swansea University Author: Mukesh Tiwari

Full text not available from this repository: check for access using links below.

DOI (Published version): 10.1145/3576915.3623141

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

Full description

Published in: Proceedings of the 2023 ACM SIGSAC Conference on Computer and Communications Security
ISBN: 979-8-4007-0050-7
Published: New York, NY, USA ACM 2023
URI: https://cronfa.swan.ac.uk/Record/cronfa65925
Tags: Add Tag
No Tags, Be the first to tag this record!
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 weapply to verify the implementations of various case study programs against a range of declassification policies.
College: Faculty of Science and Engineering
Funders: This research was sponsored by the U.S. Department of the Navy, OfficeofNavalResearch, under award N62909-18-1-2049. This material is based upon work supported by the Commonwealth of Australia Defence Science and Technology Group, Next Generation Technologies Fund (NGTF) Naumann was supported in part by NSF award CNS-1718713.

Similar Items