TYPDSEC: TYPe-based information Declassification and its SEcure Compilation

使用机密数据编程在现代世界中无处不在。例如，设想使用信用卡信息进行电子商务，使用密码或私钥进行身份验证。秘密处理代码中的错误可能导致信息泄漏，将敏感的私人信息泄露给不受信任的一方。企业往往会花费大量的资源。以确保程序处理的数据的保密性。尽管如此，攻击者还是一次又一次地设法获取敏感信息，例如，通过利用未经测试的路径或绕过部署的安全执行。据估计，到2022年，平均数据泄露造成的损失将达到435万美元。这就提出了几个基本问题，比如：1）从形式上讲，程序的安全性意味着什么？2)我们能对正在编程的数据表达保密政策吗？3)我们能建立方法来提供正式的安全保证wrt这样的机密性政策？4）最后，我们能否确保即使在编译之后也能保持这样的安全保证？(i.e.认为编译器本身没有引入一个隐蔽的通道来阻止编译前提供的保证）？该提案旨在通过构建方法和工具来回答上述问题，以提供有关程序机密性的可证明保证（即使在存在故意信息披露的情况下，这在实践中经常需要）。拟议的工作旨在实现两个关键的交付成果1。一种编程语言，其中每个程序都是通过构造可证明安全的。一种编译器，确保即使在编译之后也能保持安全保证。

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 deliverables1. 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.