A Logic for Information Security
Abstract
Software guards our most precious secrets, whether classified information on Defence networks, or your medicalhistory on your docto""r~s computer system. However, software insecurity is rife, and software borne databreaches have become increasingly common.While s""oftware insecurity has many forms, information leakage is perhaps most difficult to detect. Evenfor trivial programs it evades trad""itional program testing regimes (see Figure 1). However, confidentiality bugsneed to be found before deployment: once exploited, th""ey cannot be undone~ the cat is out of the bag.Consider the following program, wherethe integer variable secret holds someconfide""ntial information.while (secret > 0)blah secret = secret / 2;printf(""All done"");Its execution time reveals the valueblog2(secre"t)c. Discovering this requirescomparing its execution for differentvalues of secret.Figure 1: A simple timing leak.For these rea"sons, formal verification is the most effectiveway to show that programs properly keep their secrets. Onedemonstrates via a (machi""ne-checked) proof that the publiclyobservable aspects of a program~s behaviour do not depend on,and thus do no leak, secret inform"ation. In this case a program iscalled information-flow secure. The state-of-the-art remains theproofs of information-flow securit"y for micro operating systemkernels such as seL4 and CertiKOS.seL4 and CertiKOS are tiny, however, compared to everydaysoftware,"" which is immensely more complex, not least becauseit comprises many components that run concurrently to one anotherwhile sharing"" resources. Indeed, concurrency is ubiquitousin modern software systems. Despite this ubiquity, and theaforementioned verification"" successes for non-concurrent software,there exist no generally applicable logics for proving information flow security for concurr"ent programs;only highly restrictive pilots.Project Aim: To enable concurrent shared-memory programs to be proved information-flow" secure for thefirst time, by building on recent advances to develop the first generally applicable logic able to encode what itme""ans for such programs to be secure, the justification for why a particular program is secure, and to prove thisjustification is sou""nd.To do so the project will combine existing ideas from concurrent separation logic and rely-guarantee reasoning,instantiated in" the context of security-aware concurrent program semantics. It aims to develop a logicfor reasoning about potentially dynamic secu"rity properties, while allowing compositional verification of aconcurrent program (i.e. verification by reasoning about the behavio"ur of each of its concurrently-executingcomponents one-at-a-time).1
Document Details
- Document Type
- DoD Grant Award
- Publication Date
- Jan 23, 2018
- Source ID
- N629091812049
Entities
People
- Toby Murray
Organizations
- Office of Naval Research
- United States Navy
- University of Melbourne