# Academia Sinica IIS Intern [Learning] - CryptoLine
> ＣryptoLine 工具 [name=D]
- [Github](https://github.com/fmlab-iis/cryptoline)
## Introduction
- 一種能夠驗證用組合語言所寫的密碼程式（OpenSSL）的工具
- CryptoLine is a model checker that is specialized on assembly-level cryptographic libraries
- It combines the power of both **computer algebra systems** and **satisfiabilitymodulo theories solvers** to verify whether assembly programs satisfy the specified mathematical properties
## Install
```=
git clone https://github.com/fmlab-iis/cryptoline.git
sudo apt-get install opam boolector singular-ui
sudo apt install opam
opam init --disable-sandboxing
eval $(opam env)
opam install dune lwt_ppx zarith
opam install apron
opam install ppx_optcomp
```
```=
cd cryptoline
ocamlfind query zarith
```
在路徑後面加上 `/MATA` 並進行複製
```
vim ast/get-config.sh
```
```bash=
#!/bin/bash
meta=/home/demi/.opam/default/lib/zarith/META
version=$(cat ${meta} | grep -m1 "version" | cut -d "=" -f 2 | tr -d '"')
major=$(echo $version | cut -d "." -f 1)
minor=$(echo $version | cut -d "." -f 2)
echo "[%%define Z_version (${major}, ${minor})]"
```
```=
dune build
ln -s _build/default/cv.exe
./cv.exe -v -isafety examples/openssl/ecp_nistz256/ecp_nistz256_mul_mont.cl
```
## Steps
:::info
### Data Flow
簡單來說，就是先把 OpenSSL 的 library 跟 top.c 連結編譯成 執行檔，並用 `itrace.py` 轉成 assembly code，再用 `to_zdsl.py ` 轉成 CryptoLine 檔案，並且人工檢查跟更改該檔案變數名稱，等等，最後驗證 `.cl` 是否符合邏輯
:::
### make `Executable`
```=
gcc -o top top.c libcrypto.a
```
- 先利用 `gcc` 將 `top.c` 編譯成一個 binary 檔案
- `top.c` 位於 `examples/openssl/ecp_nistz256/x86_64/top.c`
- 呼叫 OpenSSL 實作函式（`ecp_nistz256_add`、`ecp_nistz256_mul_by_2`）
- `libcrpto.a` 為 OpenSSL 的 library
- 裡面包含 `top.c` 宣告的那些函式實作
:::warning
如果發生沒有此檔案或是找不到此檔案的錯誤訊息的話，可以使用以下指令
1. Install
```
$ sudo apt install libssl-dev
```
2. Find the position of the file
```
$ locate libcrpto.a
```
可以參考 [OpenSSL开发库libssl-dev的安装与应用](https://blog.csdn.net/Leon_Jinhai_Sun/article/details/139150055)
:::
### `Executable` -> ( `itrace.py` ) -> `.gas` assembly
```=
$CL_HOME/scripts/itrace.py top ecp_nistz256_add ecp_nistz256_add.gas
```
- 再利用 `itrace.py` 這個 script 將 binary 檔（`top`）裡面的 func trace 每個 register 的 address，然後生成 `.gas` 的 assembly 檔案
- `top` : first argument, the name of the executable binary
- `ecp_nistz256_add` : second argument, the name of the subroutine in the `top`
- `ecp_nistz256_add.gas` : thierd argument, the name of the output file
:::spoiler apart of `ecp_nistz256_add.gas`
```=
ecp_nistz256_add:
# %rdi = 0x7fffffffdbd0
# %rsi = 0x7fffffffdb90
# %rdx = 0x7fffffffdbb0
# %rcx = 0x7fffffffdb90
# %r8 = 0x0
# %r9 = 0x-2105ddfd00000000
#! -> SP = 0x7fffffffdb88
push %r12 #! EA = L0x7fffffffdb80; PC = 0x55555557c320
push %r13 #! EA = L0x7fffffffdb78; PC = 0x55555557c322
mov (%rsi),%r8 #! EA = L0x7fffffffdb90; Value = 0x0000000000000000; PC = 0x55555557c324
xor %r13,%r13 #! PC = 0x55555557c327
mov 0x8(%rsi),%r9 #! EA = L0x7fffffffdb98; Value = 0x0000000000000000; PC = 0x55555557c32a
mov 0x10(%rsi),%r10 #! EA = L0x7fffffffdba0; Value = 0x0000000000000000; PC = 0x55555557c32e
mov 0x18(%rsi),%r11 #! EA = L0x7fffffffdba8; Value = 0x0000000000000000; PC = 0x55555557c332
lea -0x33d(%rip),%rsi # 0x55555557c000#! PC = 0x55555557c336
```
:::
### `.gas` assembly -> ( `to_zdsl.py` ) -> `.cl` draft
```=
$CL_HOME/scripts/to_zdsl.py -r CL_HOME/scripts/x86_64.rules ecp_nistz256_add.gas > ecp_nistz256_add.cl
```
- 利用 `to_zdsl.py` 這個 script 將 組合語言的所有指令 轉成 CryptoLine 的指令，生成 `.cl` 檔案
- `to_zdsl.py`
- translation rules 可以將組語轉換成 CryptoLine 的規則
- EA : effective address of its argument
- Value : value stored in the address
- PC : program counter
:::spoiler apart of `ecp_nistz256_add.cl`
```=
proc main (%r10, %r11, %r12, %r13, %r8, %r9, %rax, %rcx, %rdi, L0x55555557c000, L0x55555557c008, L0x55555557c010, L0x55555557c018, L0x7fffffffdbb0, L0x7fffffffdbb8, L0x7fffffffdbc0, L0x7fffffffdbc8) =
{
true
&&
true
}
(* ecp_nistz256_add: *)
ecp_nistz256_add:;
(* #! -> SP = 0x7fffffffdb88 *)
#! 0x7fffffffdb88 = 0x7fffffffdb88;
(* push %r12 #! EA = L0x7fffffffdb80; PC = 0x55555557c320 *)
push %r12 #! L0x7fffffffdb80 = L0x7fffffffdb80; 0x55555557c320 = 0x55555557c320;
(* push %r13 #! EA = L0x7fffffffdb78; PC = 0x55555557c322 *)
push %r13 #! L0x7fffffffdb78 = L0x7fffffffdb78; 0x55555557c322 = 0x55555557c322;
(* mov (%rsi),%r8 #! EA = L0x7fffffffdb90; Value = 0x0000000000000000; PC = 0x55555557c324 *)
mov (%rsi),%r8 #! L0x7fffffffdb90 = L0x7fffffffdb90; 0x0000000000000000 = 0x0000000000000000; 0x55555557c324 = 0x55555557c324;
(* xor %r13,%r13 #! PC = 0x55555557c327 *)
xor %r13,%r13 #! 0x55555557c327 = 0x55555557c327;
...
(* #repz ret #! PC = 0x55555557c39c *)
#repz ret #! 0x55555557c39c = 0x55555557c39c;
{
true
&&
true
}
```
:::
### 更改 `.cl` 裡面的東西
#### proc main(...)
- this notation denotes the main subroutine in CryptoLine
- the arguments to the main subroutine are the uninitialized variables reported by `to_zdsl.py`
### 驗證 `.cl`
```=
../cv.exe -v -isafety examples/openssl/ecp_nistz256/ecp_nistz256_mul_mont.cl
```
#### CAS-based engine v.s. SMT-based engine
- CAS (Computer Algebra System)
- SMT (Satisfiability Modulo Theories)
> ```
> assert true && `<SMT>`
> assume `<CAS>` && true
> ```
```asm=
adcs carry r12 r12 rcx carry;
adc r13 r13 0x0@uint64 carry;
adcs overflow r13 r13 rbp overflow;
assert true && overflow=0@1;
assume overflow=0 && true;
```
#### algebraic v.s. range
- algebraic 代數
- 前面的部分
- 可以做加減乘除運算、mod
- range 範圍
- 後面的部分
- 只能做比較大小
> `{ <algebraic> && <range> }`
#### 驗證結果
- verifying range assertions
- assert 後面的
- verifying range specification
- postcondition 後面的
- verifying algebraic assertions
- assert 前面的
- verifying algebraic specification
- postcondition 前面的
## Examples
將驗證以下的程式碼，它們是 OpenSSL 中 NIST P-256 曲線的 x86_64 assembly code
- [CryptoLine - ecp_nistz256_add](/Iajx06FPQMe8k-alzqBUGQ)
- [CryptoLine - ecp_nistz256_sub](/RVcUYhm6TKikWj9r2XHV7g)
- [CryptoLine - ecp_nistz256_mul_mont](/qC3Qo3evSm6kOJbOrAgt6Q)
- [CryptoLine - ecp_nistz256_sqr_mont](/D_iJ_l_DRxSSWobeK17byw)
## Code
- [CryptoLine - x25519](/S59HZ79AQE-m3vl08OxGbQ)
## 一些特別且值得學習的事
- 在組語裡能發現程式碼 (**CPU 計算的部分** 和 **CPU 存放 memory 的部分**) 有交錯在一起的情形
- 原因：讓 CPU 的兩個功能能夠同步進行，使得運算時間更快
- 驗證結果的東東各代表什麼
- range assertion : assert 後面的
- range specification : postcondition 後面的
- algebraic assertions : assert 前面的
- algebraic specification : postcondition 前面的
## 相關論文
- [密碼學函式庫實作中向量化基本操作的形式驗證](https://tdr.lib.ntu.edu.tw/jspui/bitstream/123456789/88563/1/ntu-111-2.pdf)
## Reference
- [Linux 建立連結檔 ln 指令教學與範例](https://blog.gtwang.org/linux/linux-ln-command-tutorial-examples/#google_vignette)
- [函式呼叫(I) - 參數傳遞](https://sophiexin9636.github.io/posts/callfunction/)
## 感謝
- Sandy
Sign in with Wallet
Connect another wallet