No Cover Image

Conference Paper/Proceeding/Abstract 204 views

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

Toby Murray Orcid Logo, Mukesh Tiwari Orcid Logo, 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 Orcid Logo

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!
first_indexed 2024-04-03T10:16:35Z
last_indexed 2024-04-03T10:16:35Z
id cronfa65925
recordtype SURis
fullrecord <?xml version="1.0" encoding="utf-8"?><rfc1807 xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance" xmlns:xsd="http://www.w3.org/2001/XMLSchema"><bib-version>v2</bib-version><id>65925</id><entry>2024-03-28</entry><title>Assume but Verify: Deductive Verification of Leaked Information in Concurrent Applications</title><swanseaauthors><author><sid>4b6a02f9e2ebffd1dd1b7151116dd8aa</sid><ORCID>0000-0001-5373-9659</ORCID><firstname>Mukesh</firstname><surname>Tiwari</surname><name>Mukesh Tiwari</name><active>true</active><ethesisStudent>false</ethesisStudent></author></swanseaauthors><date>2024-03-28</date><deptcode>MACS</deptcode><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.</abstract><type>Conference Paper/Proceeding/Abstract</type><journal>Proceedings of the 2023 ACM SIGSAC Conference on Computer and Communications Security</journal><volume/><journalNumber/><paginationStart/><paginationEnd/><publisher>ACM</publisher><placeOfPublication>New York, NY, USA</placeOfPublication><isbnPrint/><isbnElectronic>979-8-4007-0050-7</isbnElectronic><issnPrint/><issnElectronic/><keywords/><publishedDay>21</publishedDay><publishedMonth>11</publishedMonth><publishedYear>2023</publishedYear><publishedDate>2023-11-21</publishedDate><doi>10.1145/3576915.3623141</doi><url/><notes/><college>COLLEGE NANME</college><department>Mathematics and Computer Science School</department><CollegeCode>COLLEGE CODE</CollegeCode><DepartmentCode>MACS</DepartmentCode><institution>Swansea University</institution><apcterm/><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.</funders><projectreference/><lastEdited>2024-07-11T14:21:04.4534080</lastEdited><Created>2024-03-28T07:10:28.7736856</Created><path><level id="1">Faculty of Science and Engineering</level><level id="2">School of Mathematics and Computer Science - Computer Science</level></path><authors><author><firstname>Toby</firstname><surname>Murray</surname><orcid>0000-0002-8271-0289</orcid><order>1</order></author><author><firstname>Mukesh</firstname><surname>Tiwari</surname><orcid>0000-0001-5373-9659</orcid><order>2</order></author><author><firstname>Gidon</firstname><surname>Ernst</surname><orcid>0000-0002-3289-5764</orcid><order>3</order></author><author><firstname>David A.</firstname><surname>Naumann</surname><orcid>0000-0002-7634-6150</orcid><order>4</order></author></authors><documents/><OutputDurs/></rfc1807>
spelling v2 65925 2024-03-28 Assume but Verify: Deductive Verification of Leaked Information in Concurrent Applications 4b6a02f9e2ebffd1dd1b7151116dd8aa 0000-0001-5373-9659 Mukesh Tiwari Mukesh Tiwari true false 2024-03-28 MACS 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. Conference Paper/Proceeding/Abstract Proceedings of the 2023 ACM SIGSAC Conference on Computer and Communications Security ACM New York, NY, USA 979-8-4007-0050-7 21 11 2023 2023-11-21 10.1145/3576915.3623141 COLLEGE NANME Mathematics and Computer Science School COLLEGE CODE MACS Swansea University 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. 2024-07-11T14:21:04.4534080 2024-03-28T07:10:28.7736856 Faculty of Science and Engineering School of Mathematics and Computer Science - Computer Science Toby Murray 0000-0002-8271-0289 1 Mukesh Tiwari 0000-0001-5373-9659 2 Gidon Ernst 0000-0002-3289-5764 3 David A. Naumann 0000-0002-7634-6150 4
title Assume but Verify: Deductive Verification of Leaked Information in Concurrent Applications
spellingShingle Assume but Verify: Deductive Verification of Leaked Information in Concurrent Applications
Mukesh Tiwari
title_short Assume but Verify: Deductive Verification of Leaked Information in Concurrent Applications
title_full Assume but Verify: Deductive Verification of Leaked Information in Concurrent Applications
title_fullStr Assume but Verify: Deductive Verification of Leaked Information in Concurrent Applications
title_full_unstemmed Assume but Verify: Deductive Verification of Leaked Information in Concurrent Applications
title_sort Assume but Verify: Deductive Verification of Leaked Information in Concurrent Applications
author_id_str_mv 4b6a02f9e2ebffd1dd1b7151116dd8aa
author_id_fullname_str_mv 4b6a02f9e2ebffd1dd1b7151116dd8aa_***_Mukesh Tiwari
author Mukesh Tiwari
author2 Toby Murray
Mukesh Tiwari
Gidon Ernst
David A. Naumann
format Conference Paper/Proceeding/Abstract
container_title Proceedings of the 2023 ACM SIGSAC Conference on Computer and Communications Security
publishDate 2023
institution Swansea University
isbn 979-8-4007-0050-7
doi_str_mv 10.1145/3576915.3623141
publisher ACM
college_str Faculty of Science and Engineering
hierarchytype
hierarchy_top_id facultyofscienceandengineering
hierarchy_top_title Faculty of Science and Engineering
hierarchy_parent_id facultyofscienceandengineering
hierarchy_parent_title Faculty of Science and Engineering
department_str School of Mathematics and Computer Science - Computer Science{{{_:::_}}}Faculty of Science and Engineering{{{_:::_}}}School of Mathematics and Computer Science - Computer Science
document_store_str 0
active_str 0
description 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.
published_date 2023-11-21T14:21:03Z
_version_ 1804288984439848960
score 11.035634

Similar Items