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.11 up)
- GNU Make
- OCaml packages:
dune, ocamlfind, lwt, lwt_ppx, num, zarith, ppx_optcomp - apron
- One of the following computer algebra systems:
- One of the following SMT solvers:
- abc for equivalence checking
See misc/Dockerfile.apt or misc/Dockerfile.opam for instructions to install
CryptoLine on Ubuntu 23.04.
Run the following command to see the available command-line arguments.
$ cv -help
To uninstall CryptoLine, run the following command.
$ dune uninstall
Two dockerfiles are provided in CryptoLine. Run the following commands to build a docker image and run a new container from the image.
$ docker build -t cryptoline - < misc/Dockerfile.apt
$ docker run -it --name cryptoline cryptoline bash -l
Replace misc/Dockerfile.apt with misc/Dockerfile.opam if you want to manage
OCaml packages using opam.
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.
- Vincent Hwang, Jiaxiang Liu, Gregor Seiler, Xiaomu Shi, Ming-Hsien Tsai, Bow-Yaw Wang, and Bo-Yin Yang. Verified NTT Multiplications for NISTPQC KEM Lattice Finalists: Kyber, SABER, and NTRU. IACR Transactions on Cryptographic Hardware and Embedded Systems. 2022(4): 718-750 (2022).
- 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