TYPDSEC: TYPe-based information Declassification and its SEcure Compilation

Programming with confidential data is ubiquitous in the modern world. For instance, imagine using credit card information for e-commerce, and passwords or private keys for authentication. Bugs in secret-handling code can cause information leaks, revealing sensitive, private information to untrusted parties. Corporations often spend huge amount of resources. to ensure the secrecy of the data being handled by the program. Despite all this, time-and-again attackers manage to get hold of sensitive information, for instance, by exploiting untested paths or bypassing the deployed security enforcement. The average data breach was estimated to cost USD 4.35 million in 2022. This raises several fundamental questions, like 1) What does it mean for a program to be secure in a formal sense?; 2) Can we express confidentiality policies on data being programmed?; 3) Can we build methods to provide formal security guarantees wrt such confidentiality policies? and 4) Finally, can we ensure that such security guarantees are preserved even after compilation? (i.e. argue that the compiler itself has not introduced a covert channel thwarting the guarantees offered before compilation)? The proposal aims to answer the questions like above by building methods and tools for providing provable guarantees about program confidentiality (even in the presence of deliberate information disclosure, as is often required in practice). The proposed work aims for two key deliverables 1. A programming language in which every program is provably secure by construction. 2. A compiler that ensures that security guarantees are preserved even after compilation.