TY - GEN
T1 - Assume but Verify
T2 - 30th ACM SIGSAC Conference on Computer and Communications Security, CCS 2023
AU - Murray, Toby
AU - Tiwari, Mukesh
AU - Ernst, Gidon
AU - Naumann, David A.
N1 - Publisher Copyright:
© 2023 Copyright held by the owner/author(s).
PY - 2023/11/15
Y1 - 2023/11/15
N2 - 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.
AB - 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.
KW - declassification
KW - information flow security
KW - program verification
UR - http://www.scopus.com/inward/record.url?scp=85179839615&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85179839615&partnerID=8YFLogxK
U2 - 10.1145/3576915.3623141
DO - 10.1145/3576915.3623141
M3 - Conference contribution
AN - SCOPUS:85179839615
T3 - CCS 2023 - Proceedings of the 2023 ACM SIGSAC Conference on Computer and Communications Security
SP - 1746
EP - 1760
BT - CCS 2023 - Proceedings of the 2023 ACM SIGSAC Conference on Computer and Communications Security
Y2 - 26 November 2023 through 30 November 2023
ER -