Doctoral Thesis: Confidentiality Under Nondeterminism for Storage Systems

Atalay Mert Ileri

Abstract: Storage systems are a crucial part of many software systems that store confidential data of their users. It is important to ensure that confidentiality of the stored data is maintained under many events and conditions like when a system crashes unexpectedly, in the presence of bugs, and malicious adversaries. We tackle this problem using formal verification, a technique that involves proving a software system always satisfy certain requirements.
There are numerous challenges in specifying what it means a system being confidential and proving that a system satisfies that specification: nondeterministic behavior, indirect leakage of the data, system complexity and others.
This dissertation introduces the following to address these challenges:

– Relatively deterministic noninterference, a novel confidentiality specification for storage systems with nondeterministic behavior.  Relatively deterministic noninterference accommodates discretionary access control and intentional disclosure of the system metadata.

– Nondeterminism oracles, a proof technique accompanying our specification. This technique addressed the challenges encountered in proving the confidentiality of the systems, and also reduced the proof effort required for said proofs. 

–  ConFrm, a framework that formalizes and implements nondeterminism oracles. ConFrm contains relevant metatheory to help the developer to prove that their implementation satisfies the specification.

 
 – ConFs, A confidential, crash-safe, and formally verified file system with machine-checkable proofs. ConFs uses relatively deterministic noninterference as their confidentiality specifications.

All our frameworks and systems are implemented and verified in Coq. Evaluation of our work shows relatively deterministic noninterference has 10.8x proof overhead per line of implementation code. Multiple benchmarks run on our file systems shows that ConFs is approximately 1.5 to 3 times faster than FSCQ, another verified file system with a similar design.

Details

• Date: Thursday, November 17
• Time: 1:00 pm - 2:30 pm
• Category: Thesis Defense
• Location: 32-D463

Additional Location Details:

Thesis Supervisor: Prof. Frans Kaashoek