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

TLS （Transport layer security）和SSL （secure socket layer）协议旨在在不安全的网络上建立具有保密性和完整性保证的安全通道。SSL/TLS目前被用于保护大量的服务器和网站，包括银行、文件服务器和社交网络。事实上，北美37%的网络流量现在受到SSL/TLS的保护。为了避免SSL/TLS中的冒充攻击，建议发起SSL/TLS通信的用户对其通信对等方进行身份验证，以确保他们与预期的一方而不是冒名顶替者进行交互。X.509公钥基础设施（PKI）通过提供加密支持的身份验证框架弥补了Internet固有的信任缺失，在该框架中，实体是基于信任分层组织的，每个实体都可以获得确认其身份的证书。虽然有开源软件实现了X.509规定的身份验证检查，但该软件中的错误可能会使用户容易受到冒充攻击。与SSL/TLS不同，X.509开源标准实现逃脱了严格的安全评估，尽管SSL/TLS的安全性关键取决于正确的X.509实现。该项目旨在通过开发一种自动检测X.509实现中的逻辑错误的技术，减少SSL/TLS和其他使用X.509作为身份验证提供者的应用程序的攻击面。该项目将利用给定X.509实现将证书输入域划分为接受（被实现认为有效的证书）和拒绝（被认为无效的证书）域的洞察力。可以使用符号执行从给定的X.509实现中自动提取两个宇宙的近似值，并用逻辑公式表示它们。然后，该项目旨在以某种形式逻辑精确地捕获X.509标准规范，并开发X.509标准的参考实现。为了证明参考实现对正式规范的遵从性，研究将利用模型检查和演绎验证技术的组合。R说,保证正确的参考实现,它将有可能发现逻辑错误和不一致在一个给定的x实现,T, T通过检查是否偏离了R .偏差将被有效地计算比较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.