Automating Modular Verification of Secure Information Flow

Lauren Pick, Grigory Fedyukovich, Aarti Gupta

Research output: Chapter in Book/Report/Conference proceedingConference contribution

1 Scopus citations

Abstract

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

Original languageEnglish (US)
Title of host publicationProceedings of the 20th Conference on Formal Methods in Computer-Aided Design, FMCAD 2020
EditorsAlexander Ivrii, Ofer Strichman, Warren A. Hunt, Georg Weissenbacher
PublisherInstitute of Electrical and Electronics Engineers Inc.
Pages158-168
Number of pages11
ISBN (Electronic)9783854480426
DOIs
StatePublished - Sep 21 2020
Event20th International Conference on Formal Methods in Computer-Aided Design, FMCAD 2020 - Virtual, Haifa, Israel
Duration: Sep 21 2020Sep 24 2020

Publication series

NameProceedings of the 20th Conference on Formal Methods in Computer-Aided Design, FMCAD 2020

Conference

Conference20th International Conference on Formal Methods in Computer-Aided Design, FMCAD 2020
CountryIsrael
CityVirtual, Haifa
Period9/21/209/24/20

All Science Journal Classification (ASJC) codes

  • Artificial Intelligence
  • Computer Graphics and Computer-Aided Design
  • Software
  • Safety, Risk, Reliability and Quality
  • Modeling and Simulation

Keywords

  • Formal verification
  • information security
  • model checking

Fingerprint Dive into the research topics of 'Automating Modular Verification of Secure Information Flow'. Together they form a unique fingerprint.

Cite this