ceres public version

.gitignore

@@ -0,0 +1,136 @@
+# Byte-compiled / optimized / DLL files
+__pycache__/
+*.py[cod]
+*$py.class
+
+# C extensions
+*.so
+
+# Distribution / packaging
+.Python
+build/
+develop-eggs/
+dist/
+downloads/
+eggs/
+.eggs/
+lib/
+lib64/
+parts/
+sdist/
+var/
+wheels/
+pip-wheel-metadata/
+share/python-wheels/
+*.egg-info/
+.installed.cfg
+*.egg
+MANIFEST
+
+# PyInstaller
+#  Usually these files are written by a python script from a template
+#  before PyInstaller builds the exe, so as to inject date/other infos into it.
+*.manifest
+*.spec
+
+# Installer logs
+pip-log.txt
+pip-delete-this-directory.txt
+
+# Unit test / coverage reports
+htmlcov/
+.tox/
+.nox/
+.coverage
+.coverage.*
+.cache
+nosetests.xml
+coverage.xml
+*.cover
+*.py,cover
+.hypothesis/
+.pytest_cache/
+
+# Translations
+*.mo
+*.pot
+
+# Django stuff:
+*.log
+local_settings.py
+db.sqlite3
+db.sqlite3-journal
+
+# Flask stuff:
+instance/
+.webassets-cache
+
+# Scrapy stuff:
+.scrapy
+
+# Sphinx documentation
+docs/_build/
+
+# PyBuilder
+target/
+
+# Jupyter Notebook
+.ipynb_checkpoints
+
+# IPython
+profile_default/
+ipython_config.py
+
+# pyenv
+.python-version
+
+# pipenv
+#   According to pypa/pipenv#598, it is recommended to include Pipfile.lock in version control.
+#   However, in case of collaboration, if having platform-specific dependencies or dependencies
+#   having no cross-platform support, pipenv may install dependencies that don't work, or not
+#   install all needed dependencies.
+#Pipfile.lock
+
+# PEP 582; used by e.g. github.com/David-OConnor/pyflow
+__pypackages__/
+
+# Celery stuff
+celerybeat-schedule
+celerybeat.pid
+
+# SageMath parsed files
+*.sage.py
+
+# Environments
+.env
+.venv
+env/
+venv/
+ENV/
+env.bak/
+venv.bak/
+
+# Spyder project settings
+.spyderproject
+.spyproject
+
+# Rope project settings
+.ropeproject
+
+# mkdocs documentation
+/site
+
+# mypy
+.mypy_cache/
+.dmypy.json
+dmypy.json
+
+# Pyre type checker
+.pyre/
+
+# more
+src/build
+src/bin
+*.spec
+test/differntial-testing/outputs
+test/differntial-testing/build

README.md

@@ -0,0 +1,168 @@
+# CERES
+This repository contains the official release of CERES library introduced in the paper titled *[On Re-engineering the X.509 PKI with Executable Specification for Better Implementation Guarantees](https://doi.org/10.1145/3460120.3484793)* published in 2021 ACM Conference on Computer and Communications Security (ACM CCS 2021). 
+
+## Table of Contents
+
+- [CERES](#ceres)
+  - [Table of Contents](#table-of-contents)
+  - [What is CERES?](#what-is-ceres)
+  - [Design Overview](#design-overview)
+  - [Setup](#setup)
+  - [Run](#run)
+  - [Specification Consistency](#specification-consistency)
+  - [Differential Testing](#differential-testing)
+  - [DSL-based Parser Generation](#dsl-based-parser-generation)
+  - [Datasets](#datasets)
+  - [Known Setup Issues](#known-setup-issues)
+  - [Disclaimer](#disclaimer)
+  - [Acknowledgements](#acknowledgements)
+  - [License](#license)
+  - [Citation](#citation)
+  - [Contributors](#contributors)
+
+## What is CERES?
+CERES is a high-assurance implementation of X.509 certificate chain validation logic (CCVL). This implementation is envisioned to be used as an oracle for checking noncompliance of a given CCVL implementation against the X.509 standard specification (*i.e.,* RFC 5280). One can also use CERES to validate a certificate chain to be used for configuring a TLS-enabled webserver. In addition, application developers can directly use CERES in their applications to delegate the task of X.509 certificate chain validation.
+
+## Design Overview
+CERES is realized from the following four logical modules: *Parser*, *Chain-builder*, *Driver*, and *Semantic-checker*. The *Parser* module takes as input the certificate chain to be validated as well as the trusted CA store, and returns the parse trees corresponding to the certificates. The *Chain-builder* module takes these parsed input certificates and forms candidate certificate chains. The *Semantic-checker* module then takes as input the current time, the semantic rules corresponding to the standard in Quantifier-Free First Order Logic, the ASTs corresponding to a candidate certificate chain, and the certificates in the trusted CA store, and then communicates with an "*SMT solver*" to check the assertions enforced by the semantic requirements as well as collect diagnostic information. The *Driver* module does the plumbing needed to combine the *Parser* and the *Semantic-checker* modules. Figure 1 shows the high-level design of CERES.
+
+<p align = "center">
+<img src="https://github.com/joyantaDebnath/CERES/blob/main/ceres-overview.png" width="400" height="430"></p>
+<p align = "center">Figure 1- Realization of CERES</p>
+
+## Setup
+Currently, CERES is compatible with *Linux* distributions only, and the setup script `build-ceres.sh` is tested in Ubuntu OS (version >= 16). For other *Linux* distributions, users may need to modify the  script accordingly.
+
+* To generate the CERES executable at `src/bin/ceres`, execute `build-ceres.sh`. User can optionally pass the location of trusted CA certificate store as a command-line argument in this script. Otherwise, the default *Linux* CA certificate store `/etc/ssl/certs/ca-certificates.crt` is used.
+	```
+	cd CERES/
+	./build-ceres.sh
+	```
+* To check whether CERES executable is generated successfully, execute `test/test-ceres.sh`. This script needs a directory name containing one or more X.509 certificate chains (*e.g.,* `test/sample-certs/`) as a command-line argument.
+	```
+	cd CERES/test/
+	./test-ceres.sh sample-certs/
+	```
+#### Dependencies
+* Python3
+* pip3
+* pySMT
+* CVC4
+* LFSC proof-checker
+* parsec.py
+* PyInstaller
+* GHC
+
+Note that, `build-ceres.sh` script automatically downloads and installs all these dependencies in the system before generating the CERES executable. Also, it places the *CVC4* SMT solver and *LFSC* proof-checker at `~/.ceres/extras/`.
+
+
+## Run
+* To validate an input X.509 certificate chain (**.pem** or **.crt** encoded), run the CERES executable located at `src/bin/ceres` with the given chain.
+	```
+	cd src/bin/
+	./ceres --input <input_cert_chain>
+	```
+* This is the complete list of command-line arguments supported by CERES executable.
+	```
+	--help                show manual
+	--input INPUT         input certificate chain location
+	--ca-store CA_STORE   CA certificate store location
+	--check-purpose CHECK_PURPOSE1 CHECK_PURPOSE2 ... CHECK_PURPOSEn
+	                      *** list of expected purposes of the leaf certificate: serverAuth, clientAuth, 
+	                      codeSigning, emailProtection, timeStamping, OCSPSigning, digitalSignature,
+	                      nonRepudiation, keyEncipherment, dataEncipherment, keyAgreement, keyCertSign,
+	                      cRLSign, encipherOnly, decipherOnly ***
+	--check-proof         check unsatisfiability proof
+	--show-chain          show certificate chain details
+	--check-spec          check specification consistency
+	--dsl-parser          select "dsl-based" parser instead of "parser-combinator-based" parser
+	--version             show current CERES version
+	```
+
+* The SMT-Libv2 file used by the *CVC4* SMT solver is saved in `~/.ceres/extras/CVC4/`.
+* The proof checked by the *LFSC* proof-checker is saved in `~/.ceres/extras/LFSC/`.
+
+
+## Specification Consistency
+To check specification consistency, run CERES only with `check-spec` command-line argument. This will ask the user to provide a *length* for the symbolic certificate chain. Supported chain *length* values are from 1 to 32.
+
+## Differential Testing
+Sample scripts for differential testing of CERES, GnuTLS, OpenSSL, and mbedTLS implementations (CCVL) can be found  at `test/differntial-testing/`. 
+* To run the sample differential testing script, execute the following commands.
+	```
+	cd test/differntial-testing/
+
+	# build GnuTLS, OpenSSL, and mbedTLS libraries.
+	./build-libs.sh
+
+	# run sample differential testing script
+	./diff-test.sh <directory_of_cert_chains>
+	```
+* The outputs of `diff-test.sh`  are saved in `test/differntial-testing/outputs/` for further analysis.
+
+## DSL-based Parser Generation
+The required files for automated generation of **dsl-based** parser can be found at `src/modules/parsers/dsl_based/grammar/`. User needs to run `generate-code.sh` passing a **.dsl** file that contains a grammar represented in the custom DSL discussed in the paper.
+```
+cd src/modules/parsers/dsl_based/grammar/
+./generate-code.sh <input.dsl>
+```
+
+## Datasets
+The certificate datasets used for the paper is publicly available [here](https://iowa-my.sharepoint.com/:f:/g/personal/jdebnth_uiowa_edu/EsG5_z2F3shNtqjGlhZZeKMBKK-dK3d26R58SpIvcBdfgA?e=SUgHEX). 
+Please, email at <[email protected]> if the link doesn't work.
+
+## Known Setup Issues
+* LFSC proof checker requires  `>= GLIBCXX_3.4.26`. If its missing, following commands can be issued to update `GLIBCXX`.
+	```
+	 sudo add-apt-repository ppa:ubuntu-toolchain-r/test
+	 sudo apt update
+	 sudo apt install gcc-9
+	 sudo apt install libstdc++6
+	 
+	 # check GLIBCXX version
+	 strings /usr/lib/x86_64-linux-gnu/libstdc++.so.6 | grep GLIBCXX
+	```
+* GnuTLS (v3.6.15) may fail to build due to `Libnettle 3.4.1 was not found` error. In this case, user needs to upgrade `Libnettle` to build GnuTLS for the differential testing. We found this issue only in older Ubuntu machines (e.g., `<= Ubuntu 16.04`).
+
+## Disclaimer
+
+We follow a best-effort approach to manually interpret the RFC 5280 standard and translate it into a QFFOL formula. Although our empirical evaluation gives confidence about our interpretation's correctness, "*we do not claim our interpretation to be accurate*". Hence, our interpretation should not be considered as the official interpretation intended by the RFC authors. We want to emphasize that "*CERES has not been formally proven*" to be functionally correct with respect to the standard. This is why we refrain from referring to CERES as the reference implementation and instead refer to it as a high-assurance implementation.
+
+In addition, we currently only support *RSA signature* verification. We also do not check certificate *revocation* status and do not match *hostnames*.
+
+
+## Acknowledgements
+We are grateful to [*Alan Mislove*](https://mislove.org/) for the initial idea of using measurements to drive our formalization efforts of the X.509 standard. 
+We are also thankful to [*Cesare Tinelli*](https://homepage.cs.uiowa.edu/~tinelli/) for his helpful discussions on attribute grammar and all SMT things. This work was supported by the NSF Grant CNS-2006556.
+
+## License
+Contents of this repository are restricted to non-commercial research purposes only.
+
+## Citation
+Please, use the following *bibtex* for citing this work.
+
+```
+@inproceedings{debnath2021ceres,
+	author = {Debnath, Joyanta and Chau, Sze Yiu and Chowdhury, Omar},
+	title = {On Re-engineering the X.509 PKI with Executable Specification for Better Implementation Guarantees},
+	year = {2021},
+	isbn = {9781450384544},
+	publisher = {Association for Computing Machinery},
+	address = {New York, NY, USA},
+	url = {https://doi.org/10.1145/3460120.3484793},
+	doi = {10.1145/3460120.3484793},
+	booktitle = {Proceedings of the 2021 ACM SIGSAC Conference on Computer and Communications Security},
+	pages = {17},
+	numpages = {},
+	keywords = {PKI, X.509 Certificate, Network Security, SSL/TLS Protocol, Differential Testing, Authentication, SMT Solver},
+	location = {Virtual Event, Republic of Korea},
+	series = {CCS '21}
+}
+```
+
+## Contributors
+Please, feel free to contact one of us if you have any questions.
+* [Joyanta Debnath](https://homepage.cs.uiowa.edu/~jdebnth/)
+* [Omar Chowdhury](https://homepage.divms.uiowa.edu/~comarhaider/)
+* [Sze Yiu Chau](https://szeyiuchau.github.io/)
+

build-ceres.sh

@@ -0,0 +1,29 @@
+#!/bin/bash -e
+
+cur=$(pwd)
+./cleanup.sh
+
+ca_store=${1:-"/etc/ssl/certs/ca-certificates.crt"}
+echo "CA certificate store: $ca_store"
+
+mkdir ~/.ceres/
+
+## install pre-requisite packages
+sudo apt-get update
+sudo apt-get -y install python3 python3-pip ghc libghc-regex-compat-dev libghc-text-icu-dev
+pip3 install parsec
+pip3 install pyinstaller
+pip3 install pysmt
+
+python3 src/build-ca-store.py $ca_store
+
+tar -xzf src/extras.tar.gz -C ~/.ceres/
+cd ~/.ceres/extras/stringprep
+./build.sh
+cd $cur
+
+cd src/
+python3 -m PyInstaller driver.py --onefile --name=ceres --distpath bin
+cd ..
+
+echo "Success : executable is located at CERES/src/bin/"

cleanup.sh

@@ -0,0 +1,9 @@
+#!/bin/bash
+
+rm -rf ~/.ceres/ 2> /dev/null
+
+rm -rf src/build/ 2> /dev/null
+rm -rf src/bin/ 2> /dev/null
+rm src/ceres.spec 2> /dev/null
+
+echo "Success : CERES clean up"