CryptoLine is a tool and a language for the verification of low-level implementations of mathematical constructs. It has been used to verify implementations in OpenSSL, BoringSSL, mbed TLS, pqm4, ntt-polymul, etc.
To compile and run CryptoLine, the following packages need to be installed.
- OCaml compiler (version 4.08.1 up)
- GNU Make
- OCaml packages: dune, ocamlfind, lwt, lwt_ppx, num, zarith
- One of the following computer algebra systems:
- One of the following SMT solvers:
Follow the following instructions to build and install CryptoLine as well as the default solver Singular and Boolector on Ubuntu 20.04 LTS.
$ sudo apt -y install \
build-essential ocaml ocaml-dune libzarith-ocaml-dev liblwt-ocaml-dev \
boolector singular
$ dune build
$ dune install
Run the following command to see the available command-line arguments.
$ cv -help
To uninstall CryptoLine, run the following command.
$ dune uninstall
Note that Singular and Boolector provided by Ubuntu are pretty old. It is recommended to install newer versions of Singular and Boolector. Using the scripts install-singular.sh and install-boolector.sh, Singular 4.1.3p2 and Boolector 3.2.0 can be installed.
$ scripts/install-singular.sh
$ scripts/install-boolector.sh
To test the installation of CryptoLine, run the following command in the project root.
$ ./run_experiments -simple
Below is the expected output (time may vary).
Verifying examples/qhasm/fe25519_add.cl: 0 seconds [OK]
Verifying examples/qhasm/fe25519_sub.cl: 1 seconds [OK]
Verifying examples/qhasm/fe25519r64_add.cl: 0 seconds [OK]
Verifying examples/qhasm/fe25519r64_addsub.cl: 0 seconds [OK]
Verifying examples/qhasm/fe25519r64_sub.cl: 0 seconds [OK]
Verify a CryptoLine program program.cl.
$ cv program.cl
Parse a CryptoLine program program.cl.
$ cv -p program.cl
Output the SSA (Static Single Assignment) form of a CryptoLine program program.cl.
$ cv -pssa program.cl
Verify a CryptoLine program program.cl with at most 2 parallel jobs (-jobs 2), verbose outputs (-v), incremental checking of algebraic soundness (-isafety), and program slicing (-slicing).
$ cv -v -jobs 2 -isafety -slicing program.cl
Read doc/cryptoline.pdf for the details of the CryptoLine language.
A tutorial of CryptoLine is available in doc/tutorial.pdf.
Syntax highlighting in Emacs is provided by misc/cryptoLine-mode.el.
; Change [PATH_TO_CRYPTOLINE] to the right location
(add-to-list 'load-path "[PATH_TO_CRYPTOLINE]/misc")
(autoload 'cryptoline-mode "cryptoline-mode" "Major mode for CryptoLine files." t)
(add-to-list 'auto-mode-alist '("\\.cl\\'" . cryptoline-mode))Syntax highlighting in Visual Studio Code is provided by the extension misc/cryptoline-vscode-extension/cryptoline-x.y.z.vsix where x.y.z is the version of the extension.
- Yu-Fu Fu, Jiaxiang Liu, Xiaomu Shi, Ming-Hsien Tsai, Bow-Yaw Wang, and Bo-Yin Yang. Signed Cryptographic Program Verification with Typed CryptoLine. In Proceedings of the 2019 ACM SIGSAC Conference on Computer and Communications Security (CCS '19). ACM, New York, NY, USA, 1591-1606. DOI: https://doi.org/10.1145/3319535.3354199
- Andy Polyakov, Ming-Hsien Tsai, Bow-Yaw Wang, Bo-Yin Yang: Verifying Arithmetic Assembly Programs in Cryptographic Primitives (Invited Talk). International Conference on Concurrency Theory (CONCUR), 4:1-4:16, LIPIcs, 2018
- Ming-Hsien Tsai, Bow-Yaw Wang, Bo-Yin Yang: Certified Verification of Algebraic Properties on Low-Level Mathematical Constructs in Cryptographic Programs. ACM SIGSAC Conference on Computer and Communications Security (CCS), pp. 1973-1987, ACM, 2017
- Yu-Fang Chen, Chang-Hong Hsu, Hsin-Hung Lin, Peter Schwabe, Ming-Hsien Tsai, Bow-Yaw Wang, Bo-Yin Yang, Shang-Yi Yang: Verifying Curve25519 Software. ACM SIGSAC Conference on Computer and Communications Security (CCS), pp. 299-309, ACM, 2014