| NSF Org: |
CNS Division Of Computer and Network Systems |
| Recipient: |
|
| Initial Amendment Date: | January 25, 2017 |
| Latest Amendment Date: | January 25, 2017 |
| Award Number: | 1657124 |
| Award Instrument: | Standard Grant |
| Program Manager: |
Phillip Regalia
pregalia@nsf.gov (703)292-2981 CNS Division Of Computer and Network Systems CSE Directorate for Computer and Information Science and Engineering |
| Start Date: | June 1, 2017 |
| End Date: | August 31, 2020 (Estimated) |
| Total Intended Award Amount: | $174,958.00 |
| Total Awarded Amount to Date: | $174,958.00 |
| Funds Obligated to Date: |
|
| History of Investigator: |
|
| Recipient Sponsored Research Office: |
105 JESSUP HALL IOWA CITY IA US 52242-1316 (319)335-2123 |
| Sponsor Congressional District: |
|
| Primary Place of Performance: |
14 MacLean Hall Iowa city IA US 52242-1419 |
| Primary Place of
Performance Congressional District: |
|
| Unique Entity Identifier (UEI): |
|
| Parent UEI: |
|
| NSF Program(s): | CRII CISE Research Initiation |
| Primary Program Source: |
|
| Program Reference Code(s): |
|
| Program Element Code(s): |
|
| Award Agency Code: | 4900 |
| Fund Agency Code: | 4900 |
| Assistance Listing Number(s): | 47.070 |
ABSTRACT
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.
PUBLICATIONS PRODUCED AS A RESULT OF THIS RESEARCH
Note:
When clicking on a Digital Object Identifier (DOI) number, you will be taken to an external
site maintained by the publisher. Some full text articles may not yet be available without a
charge during the embargo (administrative interval).
Some links on this page may take you to non-federal websites. Their policies may differ from
this site.
PROJECT OUTCOMES REPORT
Disclaimer
This Project Outcomes Report for the General Public is displayed verbatim as submitted by the Principal Investigator (PI) for this award. Any opinions, findings, and conclusions or recommendations expressed in this Report are those of the PI and do not necessarily reflect the views of the National Science Foundation; NSF has not approved or endorsed its content.
This project focused on developing an automatic testing approach for checking compliance of an X.509 Public Key Infrastructure (PKI) implementation with RFC 5280. The tools and foundational techniques developed in this project can identify noncompliances during the early development stage of implementation. This way, it is possible to avoid the security repercussions of non-compliance during deployment. The testing approach comprises of two logical components: (a) a testing approach that can find behavioral deviations of two different X.509 implementations using symbolic execution; (b) a reference implementation that faithfully follows the requirements of RFC 5280. For testing the compliance of a given implementation s, one would use component (a) to test the deviations between s and the reference implementation developed in (b).
In this project, as part of component (a) mentioned above, we developed an open-source tool to generate a custom certificate chain containing concrete and symbolic values, called SymCert. The next component of (a) then uses such SymCerts for symbolically executing an implementation under test for approximating the logic. The final component of (a) uses a satisfiability modulo theory (SMT) solver to compare the extracted logic of two different implementations. Our evaluation demonstrates that this approach can recognize differences between implementations that are hard for fuzzing based techniques to discover. Additionally, for testing the PKCS#1 v1.5 signature verification checks, performed as part of certificate chain validation, we developed an automatic, custom tool that uses a two-stage search combining brute-force and symbolic execution. This tool includes a constraint provenance tracker (CPT) that keeps track of the source code fragment that contributed to a particular constraint during symbolic execution. The evaluation of these tools with real open-source cryptographic libraries have discovered real vulnerabilities and noncompliances that have been fixed by the stakeholders.
For component (b), dubbed CERES, the project takes a different approach than a typical workflow used for developing a formally verified implementation. In CERES, we use the novel notion of executable specification, which allows a custom interpreter to execute the specification directly and consequently giving us a reference implementation with little to no cost. We observed that it is possible to develop such an executable specification for X.509 standard. Such a specification is feasible due to the partitioning of the specification into syntactic and semantic rules. For capturing the syntactic requirements of an X.509 certificate according to RFC 5280, we use a restricted fragment of the attribute grammar. This identified fragment of attribute grammar induces efficient parsers that do not require backtracking. For capturing semantic restrictions, we observed that a quantifier-free first-order logic (QF-FOL) fragment is sufficient. An SMT solver can thus check semantic requirements expressed in this QF-FOL fragment. Using an SMT solver for checking semantic requirements has the following benefits: (I) it is possible to check the absence of conflicting requirements; (II) the SMT solver can provide the causes and proof of non-compliance; (III) one can easily extend the semantic requirements to add newer requirements with little cost. An empirical evaluation comparing CERES and other open-source cryptographic libraries show that CERES is more restrictive while generating rich diagnostic information of non-compliance.
Along with the aforementioned technical innovations and open-source tools, the project has enabled and inspired the PI to pursue the relevant area of the practical deployment challenges of a PKI. In the context of SSL/TLS, we developed testing platforms that can check whether a mobile app or data-saving-web-browser faithfully establishes an SSL/TLS connection in the presence of a proxy. Our testing platforms revealed severe weaknesses of the mobile data-saving-web-browsers that can jeopardize user's security and privacy. Also, this project has supported the development of cellular network protocol testers like LTEInspector and 5GReasoner. These two tools have helped us discover real vulnerabilities in the cellular network protocols and have induced changes to the protocol standard.
This project has helped the PI train three different students in the early stages of their Ph.D. careers, among which one of them is under-represented. The tools and techniques developed in this project have contributed materials to the curriculum of an advanced topic on security and privacy course taught by the PI. The results of this project have been disseminated in research manuscripts published in top-tier security venues. All the software artifacts will be available with open-source licenses from the PI's institutional webpage: https://homepage.divms.uiowa.edu/~comarhaider/NSFPKI/index.html
Last Modified: 12/30/2020
Modified by: Omar Haider Chowdhury
Please report errors in award information by writing to: awardsearch@nsf.gov.
