Skip to main content

Automating Modular Verification of Secure Information Flow

Author(s): Pick, Lauren; Fedyukovich, Grigory; Gupta, Aarti

Download
To refer to this page use: http://arks.princeton.edu/ark:/88435/pr1sk1h
Full metadata record
DC FieldValueLanguage
dc.contributor.authorPick, Lauren-
dc.contributor.authorFedyukovich, Grigory-
dc.contributor.authorGupta, Aarti-
dc.date.accessioned2021-10-08T19:51:02Z-
dc.date.available2021-10-08T19:51:02Z-
dc.date.issued2020en_US
dc.identifier.citationPick, Lauren, Grigory Fedyukovich, and Aarti Gupta. "Automating Modular Verification of Secure Information Flow." In Proceedings of the 20th Conference on Formal Methods in Computer-Aided Design (2020): pp. 158-168. doi: 10.34727/2020/isbn.978-3-85448-042-6_23en_US
dc.identifier.urihttp://arks.princeton.edu/ark:/88435/pr1sk1h-
dc.description.abstractVerifying secure information flow by reducing it to safety verification is a popular approach, based on constructing product programs or self-compositions of given programs. However, most such existing efforts are non-modular, i.e., they do not infer relational specifications for procedures in interprocedural programs. Such relational specifications can help to verify security properties in a modular fashion, e.g., for verifying clients of library APIs. They also provide security contracts at procedure boundaries to aid code understanding and maintenance. There has been recent interest in constructing modular product programs, but where users are required to provide procedure summaries and related annotations. In this work, we propose to automatically infer relational specifications for procedures in modular product programs. Our approach uses syntax-guided synthesis techniques and grammar templates that target verification of secure information flow properties. This enables automation of modular verification for such properties, thereby reducing the annotation burden. We have implemented our techniques on top of a solver for constrained Horn clauses (CHC). Our evaluation demonstrates that our tool is capable of inferring adequate relational specifications for procedures without requiring annotations. Furthermore, it outperforms an existing state-of-the-art hyperproperty verifier and a modular CHC-based verifier on benchmarks with loops or recursion.en_US
dc.format.extent158 - 168en_US
dc.language.isoen_USen_US
dc.relation.ispartofProceedings of the 20th Conference on Formal Methods in Computer-Aided Designen_US
dc.rightsFinal published version. This is an open access article.en_US
dc.titleAutomating Modular Verification of Secure Information Flowen_US
dc.typeConference Articleen_US
dc.identifier.doi10.34727/2020/isbn.978-3-85448-042-6_23-
dc.identifier.eissn2708-7824-
pu.type.symplectichttp://www.symplectic.co.uk/publications/atom-terms/1.0/conference-proceedingen_US

Files in This Item:
File Description SizeFormat 
AutomatingModularVerif.pdf510.46 kBAdobe PDFView/Download


Items in OAR@Princeton are protected by copyright, with all rights reserved, unless otherwise indicated.