Assume but Verify: Deductive Verification of Leaked Information in Concurrent Applications (Extended Version)

TL;DR

This paper introduces a deductive verification method for concurrent programs that leak information intentionally, combining program logic extension and policy auditing to ensure security properties are maintained.

Contribution

It extends existing program logic SecCSL to verify controlled information leaks and provides a formal framework for auditing declassifications against security policies.

Findings

Successfully verified concurrent programs against declassification policies

Extended SecCSL logic to enforce leak restrictions

Applied methodology to real case studies with positive results

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.