# Academia Sinica IIS Intern [Learning] - CryptoLine > [name=D] ## Doc - [Github](https://github.com/fmlab-iis/cryptoline) - [相關論文](https://tdr.lib.ntu.edu.tw/jspui/bitstream/123456789/88563/1/ntu-111-2.pdf) ## Introduction - 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 - 一種能夠驗證用組合語言所寫的密碼程式的工具 ## Steps ### make `Executable` > `gcc -o top top.c libcrypto.a` - 先利用 `gcc` 將 C 語言的程式碼編譯成一個 Binary 檔案 - `libcrpto.a` 為 OPENSSL 套件 - 如果發生沒有此檔案或是找不到此檔案的錯誤訊息的話，可以使用以下指令 - `$ sudo apt install libssl-dev` : Install - `$ locate libcrpto.a` : Find the position of the file ### `Executable` -> ( `itrace.py` ) -> `.gas` assembly > `$CL_HOME/scripts/itrace.py top ecp_nistz256_add ecp_nistz256_add.gas` - 再利用 `itrace.py` 這個 script 將 副程式 trace 每個 register 的 address，然後生成 `.gas` 的檔案 - `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 #### algebraic v.s. range > `{ <algebraic> && <range> }` - algebraic 代數 - 前面的部分 - 可以做加減乘除運算、mod - range 範圍 - 後面的部分 - 只能做比較大小的部分 #### 驗證結果 - verifying range assertions - assert 後面的 - verifying range specification - postcondition 後面的 - verifying algebraic assertions - assert 前面的 - verifying algebraic specification - postcondition 前面的 ### Data Flow ![image](https://hackmd.io/_uploads/HkkOa9oDA.png =350x) ## 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 ``` ## Examples - [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 前面的 ## Reference - [Linux 建立連結檔 ln 指令教學與範例](https://blog.gtwang.org/linux/linux-ln-command-tutorial-examples/#google_vignette) - [函式呼叫(I) - 參數傳遞](https://sophiexin9636.github.io/posts/callfunction/) ## 感謝 - Sandy