TYPDSEC: TYPe-based information Declassification and its SEcure Compilation

在现代世界中，使用机密数据进行编程是无处不在的。例如，设想使用信用卡信息进行电子商务，并使用密码或私钥进行身份验证。秘密处理代码中的错误可能会导致信息泄漏，将敏感的私人信息泄露给不受信任的各方。企业往往会花费大量资源。以确保程序正在处理的数据的保密性。尽管如此，一次又一次的攻击者设法获得敏感信息，例如，通过利用未经测试的路径或绕过部署的安全实施。据估计，2022年数据泄露的平均成本为435万美元。这引发了几个基本问题，如1)程序在正式意义上是安全的意味着什么？2)我们可以对正在编程的数据表达保密政策吗？3)我们能否建立方法来提供正式的安全保证WRT这样的保密政策？以及4)最后，我们能否确保即使在编译之后也能保留这样的安全保证？(即，争辩编译器本身没有引入秘密通道来阻挠编译前提供的保证)？该提案旨在通过构建方法和工具来回答上述问题，以提供关于程序机密性的可证明保证(即使在存在故意信息泄露的情况下也是如此，正如实践中经常需要的)。拟议的工作旨在实现两项关键成果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.