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

Murray, Toby ; Tiwari, Mukesh ; Ernst, Gidon und Naumann, David A. (2023): Assume but Verify: Deductive Verification of Leaked Information in Concurrent Applications. 30th ACM SIGSAC Conference on Computer and Communications Security (ACM CCS), Copenhagen, Denmark, 26. - 30. November 2023. Meng, Weizhi und Jensen, Christian D. (Hrsg.): In: Proceedings of the 2023 ACM SIGSAC Conference on Computer and Communications Security, New York: Association for Computing Machinery. S. 1746-1760

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.

• Dokumententyp: Konferenzbeitrag (Paper)
• Fakultät: Mathematik, Informatik und Statistik > Informatik
• Themengebiete: 000 Informatik, Informationswissenschaft, allgemeine Werke > 004 Informatik
• ISBN: 979-8-4007-0050-7
• Ort: New York
• Sprache: Englisch