CRII: SaTC: A Principled Approach Aiding the Development of a Compliant Internet PKI

传输层安全(TLS)和安全套接字层(SSL)协议旨在通过不安全的网络建立具有机密性和完整性保证的安全通道。目前，SSL/TLS被用来保护大量服务器和网站，包括银行、文件服务器和社交网络。事实上，北美37%的网络流量现在受到SSL/TLS的保护。为了避免SSL/TLS中的模拟攻击，建议发起SSL/TLS通信的用户对其通信对等方进行身份验证，以确保他们正在与目标方交互，而不是冒名顶替者。X.509公钥基础设施(PKI)通过提供密码支持的身份验证框架来弥补互联网固有的信任缺失，在该框架中，实体基于信任被分层组织，并且每个实体都可以获得确认其身份的证书。虽然有实现X.509规定的身份验证检查的开源软件，但该软件中的错误可能会使用户容易受到模拟攻击。与SSL/TLS不同，X.509开源标准实现逃脱了严格的安全评估，尽管SSL/TLS的安全性在很大程度上取决于正确的X.509实现。该项目寻求通过开发一种自动技术来检测X.509实现中的逻辑错误，从而减少使用X.509作为身份验证提供者的SSL/TLS和其他应用程序的攻击面。这个项目将利用这样一种见解，即给定的X.509实现将证书输入领域划分为接受(实现认为有效的证书)和拒绝(证书认为无效)领域。可以使用符号执行从给定的X.509实现中自动提取两个宇宙的近似值，并用逻辑公式表示它们。然后，该项目的目标是在一些形式逻辑中准确地捕获X.509标准规范，并开发X.509标准的参考实现。为了证明参考实现与形式规范的一致性，研究将利用模型检查和演绎验证技术的组合。利用手头的可证明正确的参考实现，例如R，将可能通过检查T是否偏离R来检测给定X.509实现T中的逻辑错误和不一致。将通过比较R和T的证书领域来有效地计算偏离。除了其研究影响之外，该项目的技术和研究成果将对下一代计算机安全专业人员的培训产生积极影响。

Transport layer security (TLS) and secure socket layer (SSL) protocols aim to establish a secure channel with confidentiality and integrity guarantees over an insecure network. SSL/TLS is currently being used to protect a large number of servers and websites including banks, file servers, and social networks. In fact, 37% of North America's network traffic is now protected by SSL/TLS. To avoid impersonation attacks in SSL/TLS, users initiating an SSL/TLS communication are recommended to authenticate their communication peer to ensure they are interacting with the intended party and not an impostor. The X.509 public-key infrastructure (PKI) compensates for the Internet's inherent lack of trust by providing a cryptography-backed authentication framework in which entities are organized hierarchically based on trust, and each entity can obtain a certificate confirming its identity. While there is open-source software that implements the X.509 prescribed authentication checks, bugs in this software can leave users vulnerable to impersonation attacks. The X.509 open-source standard implementations, unlike SSL/TLS, have escaped rigorous security evaluations despite the fact that the security of SSL/TLS critically hinges on a correct X.509 implementation. This project seeks to reduce the attack surface of SSL/TLS and other applications that use X.509 as the authentication provider by developing an automatic technique for detecting logical bugs in X.509 implementations. This project will take advantage of the insight that a given X.509 implementation partitions the certificate input universe into accepting (certificates considered valid by the implementation) and rejecting (certificates considered invalid) universes. One can use symbolic execution to automatically extract an approximation of the two universes from a given X.509 implementation and represent them with logical formulas. The project then aims to precisely capture the X.509 standard specification in some formal logic and also develop a reference implementation of the X.509 standard. To prove the compliance of the reference implementation against the formal specification, the research will leverage a combination of model checking and deductive verification techniques. With the provably correct reference implementation, say R, at hand, it will be possible to detect logical bugs and inconsistencies in a given X.509 implementation, T, by checking whether T deviates from R. Deviations will be efficiently calculated by comparing the certificate universes of R and T. In addition to its research impact, the techniques and research findings of this project will have a positive impact on the training of the future generation of computer security professionals.