Skip to content

README.md

Latest commit

 

History

History
117 lines (65 loc) · 3.16 KB

README.md

File metadata and controls

117 lines (65 loc) · 3.16 KB

llvm2cryptoline

Introduction

Cryptographic primitives are the basic blocks of cryptosystems and Contains a large number of arithmetic operations over large finite fields that are difficult to verify. llvm2cryptoline is a formal verification tool verify the functional correctness of cryptographic programs implemented in C.

A video demonstration is available at https://youtu.be/QXuSmja45VA

Installation

Requirements

  1. cmake (>= 3.7, lower version may be viable, you are welcomed to have a try)
  2. LLVM (14.0.0)
  3. ANTLR4 tool (4.12.0)

NOTE: the LLVM version used for compiling llvm2cryptoline SHOULD be the same as the one corresponding to the IR code.

LLVM Installation

NOTE: If you have already installed LLVM, you can skip this part.

WAY1: Install precompiled binaries:

  1. Download the binaries of the release at https://github.com/llvm/llvm-project/releases

  2. Unzip and put it somewhere the system can find.

  3. Add the installation directory to the PATH environment variable.

WAY2: Compile and install:

  1. Download LLVM source code from http://releases.llvm.org/download.html

  2. Extract the source code from the downloaded package. Assume that the top-level directory of the source code is SRC_ROOT.

  3. Enter BUILD_DIR, where you want to build your LLVM. For example, create directory SRC_ROOT/build and enter in:

    cd SRC_ROOT mkdir build && cd build

  4. Assume that you want to install LLVM into the directory INSTALL_DIR, then:

    cmake -DCMAKE_INSTALL_PREFIX=INSTALL_DIR SRC_ROOT

    For example, if you are in SRC_ROOT/build, you can:

    cmake -DCMAKE_INSTALL_PREFIX=INSTALL_DIR ..

  5. Build:

    make

    Or use n processors to speed up:

    make -jn

  6. Install:

    make install

  7. Now you can delete all files in SRC_ROOT and BUILD_DIR.

llvm2cryptoline Compilation

Assume that SRC_ROOT is the top-level directory of the llvm2cryptoline source code, LLVM_INSTALL_DIR is the directory where you installed your LLVM (i.e. INSTALL_DIR in the previous part), and your ANTLR4 tool in the directory ANTLR_DIR.

  1. cd SRC_ROOT

  2. mkdir build && cd build

  3. cmake -DLLVM_DIR=LLVM_INSTALL_DIR/lib/cmake/llvm/ -DANTLR_EXECUTABLE=ANTLR_DIR/antlr-4.12.0-complete.jar ..

  4. make

llvm2cryptoline Usage

Use the following command line:

$ verify <FILE>  <FUNCTION_NAME> <SPECIFICATION> [OPTIONS]

- FILE		            the LLVM IR code (.ll) file

- FUNCTION_NAME         the verified function name

- SPECIFICATION	        the properties of the program (.spec)

- OPTIONS       	    optional parameters

Options:

  • -block <b>: translate the block in the target IR function;
  • -disable_heuristic: disable heuristics
  • -disable_cryptoline: disable the invocation of the Cryptoline tool
  • -enable_aggr_heuristic: enable the aggressive heuristcs
  • enable_aggr_shl: enable the aggressive translation of the IR instruction {shl}
  • -save_cryptoline: save the generated Cryptoline problem (.cl)
  • -type <type>: specify the default type for translation, which can be signed or unsigned (the default)
  • -v: display verbose messages output by Cryptoline
  • -h: Print this help info