Maintaining the security of data is an essential property of many computer programs. Developers working on projects which manage confidential information will often outline “policies” which dictate how and when a program can interact with and disseminate confidential information. But how can they be certain that their program conforms to these policies?
The most common strategy for assessing whether a program satisfies security policies is with test cases – a finite number of manual constructed examples which are executed and analyzed. But unless the entire space of possible inputs to a program can be feasibly covered with test cases – which is rare – test cases can only grant confidence, not certainty, that a program is working as expected.
In a research project during the summer of 2020, I contributed to a modern strategy for examining programs and their adherence to confidentiality policies. I call this strategy CETA, or Confidentiality Enforcement via Type Abstraction. This programming paradigm allows a developer to pragmatically encode their security policies directly into the code they are writing, in such a way that the code will only compile and execute if the policies are satisfied. CETA is explained in more detail in the research poster below.
CETA suffers an interesting issue, one which is fundamental to all of programming at varying degrees of severity. The question is, just because I’ve programmed something which runs successfully, how can I be sure I’ve programmed the thing I intended to program? Translating a thought, a mental algorithm, into code is not always an obvious process. With a paradigm like CETA, where policies are woven directly and obtusely into the code, it’s hard to be certain you’ve truly captured the correct policies in your code.
Skip to PDF content