# 自我檢查 ( Sandbox )
contributed by <`williamchangTW`>
###### tags: `Class_Project`, `Jserv`

---
## 隔離執行環境的建構
---
- [x] 自我檢查項目
- [x] Trusted Execution Environment (TEE) 的應用為何？(舉出共筆以外的真實世界案例)
- [TEE](https://en.wikipedia.org/wiki/Trusted_execution_environment) 是在不安全的作業環境下，建構獨立執行環境，解決行動裝置之軟體執行安全性問題。須有獨立硬體，以提供安全的作業系統、程式、使用介面、資料儲存空間等，不是在裝置的作業系統上運作。
- 有(除了共筆外)：
- 數位版權管理 :
- 音樂及影片內容容易被破解，可利用 TEE 的 Trusted application 來提供安全的運作，例如: [TrustZone](https://www.arm.com/files/event/Developer_Track_6_TrustZone_TEEs_and_Trusted_Video_Path_implementation_considerations.pdf)
- 企業應用 :
- 遠端存取資料及 Secure VPN 與動態密碼使用等作業系統安全須受到嚴格的檢視，TEE 是個良好的解決方法
- [x] 是否已詳細閱讀 [Moxie](http://moxielogic.org/blog/) 處理器架構的 [Architecture](http://moxielogic.org/blog/pages/architecture.html) 文件？能否用 Moxie 組合語言寫出迴圈版本的 Fibonacci 數列程式？
- 用組合語言呈現 Fabonnaci(set loop 10 times )
- `rtes@rtes-Aspire-M1470-V:~/build-toolchain/moxiebox/tests$ moxie-none-moxiebox-gcc -I../runtime -Wall -Os -S -g -pipe -fno-stack-protector -ffunction-sections -fdata-sections -fno-asynchronous-unwind-tables -c Fibonnaci.c
` 研究過後使用這個指令產生 assembly code
~~~assembly
.file "Fibonnaci.c"
.text
.Ltext0:
.section .text.Fibonnaci,"ax",@progbits
.p2align 1
.global Fibonnaci
.type Fibonnaci, @function
Fibonnaci:
.LFB3:
.LM1:
.LVL0:
mov $r3, $r0
.LVL1:
.LM2:
ldi.l $r2, 1
.LM3:
mov $r0, $r2
.LVL2:
.LM4:
xor $r1, $r1
.LVL3:
.L2:
.LM5:
cmp $r3, $r1
bgeu .L3
.LM6:
ret
.L3:
.LVL4:
.LM7:
mov $r4, $r0
add $r4, $r2
.LVL5:
.LM8:
inc $r1, 1
.LVL6:
mov $r2, $r0
.LM9:
mov $r0, $r4
.LVL7:
jmpa .L2
.LFE3:
.size Fibonnaci, .-Fibonnaci
.section .rodata.main.str1.4,"aMS",@progbits,1
.p2align 2
.LC0:
.string "Fibonnaci in the number 10 is : %d\n"
.section .text.startup.main,"ax",@progbits
.p2align 1
.global main
.type main, @function
main:
.LFB4:
.LM10:
dec $sp, 24
.LCFI0:
.LVL8:
.LM11:
ldi.l $r0, 10
jsra Fibonnaci
.LVL9:
mov $r1, $r0
ldi.l $r0, .LC0
jsra printf
.LVL10:
.LM12:
xor $r0, $r0
ret
.LFE4:
.size main, .-main
.section .debug_frame,"",@progbits
.Lframe0:
.4byte .LECIE0-.LSCIE0
.LSCIE0:
.4byte 0xffffffff
.byte 0x3
.string ""
.uleb128 0x1
.sleb128 -4
.uleb128 0x14
.byte 0xc
.uleb128 0x1
.uleb128 0
.byte 0x11
.uleb128 0x14
.sleb128 -1
.p2align 2
.LECIE0:
~~~
>fibonnaci.c file content:
~~~c
#include <stdlib.h>
#include <stdio.h>
int Fibonnaci(unsigned int i) {
int w, z;
int x = 1;
int y = 1;
for (z = 0; z <= i; z++) {
w = x;
x = x + y;
y = w;
}
return x;
}

int main() {
int i = 10;
Fibonnaci(i);
printf("Fibonnaci in the number 10 is : %d\n", Fibonnaci(i));
return 0;
}
~~~
- [ ] binutils, gcc, glibc, qemu 到 [libffi](https://sourceware.org/libffi/) 這些專案的作用為何？
- [x] Intel 的 [Software Guard Extensions](https://software.intel.com/en-us/sgx) 關鍵特性為何？並舉出共筆以外的應用案例
* intel [Software Guard Extensions](https://software.intel.com/en-us/sgx) 是在一塊受保護的記憶體中執行應用程式的 code
* 以下參考：[加密貨幣硬體錢包公司 Ledger 與英特爾合作 將 SGX 技術整合進產品當中](http://blockcast.it/2017/10/25/intel-partners-with-ledger-to-integrate-bitcoin-wallet-software-and-sgx-tech/)
* **私鑰的儲存**以及**交易產生的簽名**都在 SGX 的安全區域內
* 解決在區域鏈所發生的問題，比如**比特幣**，若**比特幣**被偷了，就是消失無蹤了。**比特幣就是私鑰**，也是交易的關鍵訊息，若有人可以知道你的私鑰，那他就可以擁有它
* 資料參考：[Signal taps up Intel's SGX to (hopefully) stop contacts falling into hackers, cops' hands](https://www.theregister.co.uk/2017/09/27/signal_turns_to_intels_sgx_to_lock_down_contacts_from_spying_eyes/)
* 應用：[Fortanix](https://www.fortanix.com/products/sdkms/)
* 最難去攻擊的地方，是當攻擊者擁有的你 root password ，則所有的資料將如裸露一般的讓攻擊者任意去操控。可以擁有你的資料或 IP address ，則如果攻擊者有你的 root password 則這世上沒有任何一個防護工具可以防護。
* 有鑑於此，所以提出了一個 Runtime encryption 去保護資料，其中便使用了 Intel 的 [Software Guard Extensions](https://software.intel.com/en-us/sgx) ，用有後面所述的好處
* 可以隨時隨地的保護資料
* 沒有 [Zero-day bug](https://en.wikipedia.org/wiki/Zero-day_(computing)) 的問題
* 沒有侵入者想侵入網路所造成的損失，或者是說沒有機會讓侵入者攻擊
* 無法取得 root password 能竊取所有能動用的資源
* [Fortanix](https://www.fortanix.com/products/sdkms/) 這個產品使用了 Fortanix Self-Defending Key Management Service (SDKMS) 這個技術去防護資料竊取，這是一種雲端防護服務使用Intel 的 [Software Guard Extensions](https://software.intel.com/en-us/sgx)去當硬體基底也是第一個。在這項技術下，你可以秘密的使用密鑰 (also can generate and store) 就像密碼一樣，或是 [API keys](https://stackoverflow.com/questions/1453073/what-is-an-api-key)等...。
* 文中有提到這個產品的競爭力，舉了一個例子，說道當一個推銷員推銷一個防護產品，只有 post-breach notification 的功能，也就是說，當一個人闖入你家時會提醒你他闖入你家**而已**，**可是他已經可以動用你家裡的東西了**，這樣你大概不會想要買這項產品，而 [Fortanix](https://www.fortanix.com/products/sdkms/) 就是預防他進入你家
* 文獻中有提及可以使用在 IOT 及 [PKI(Public key infrastructure)](https://en.wikipedia.org/wiki/Public_key_infrastructure) 中

* 參考資料：
* [Fortanix Creates A New Industry Category Using Intel SGX – Runtime Encryption](https://www.superbcrew.com/fortanix-creates-a-new-industry-category-using-intel-sgx-runtime-encryption/)
* [Fortanix Has Series A Funding for Run-Time Encryption](https://www.securitynow.com/author.asp?section_id=654&doc_id=736806)
* [Fortanix](https://www.fortanix.com/products/sdkms/)
>這裡對 [Software Guard Extensions](https://software.intel.com/en-us/sgx) 思考：把這個觀念簡易化，舉例如果這個世界上銀行體系不值得信任時，所有的錢可能會變成現金在身上不會存在銀行中，而這個技術似乎就是朝這個方向所做的產品，不管虛擬還實體上都是一個對他基於信任基礎與共同的認同上才具備其效力。
- [ ] [moxiebox](https://github.com/sysprog21/moxiebox) 打造出隔離執行 (sandbox) 的運作環境該如何與外界溝通？列出對應的程式碼並解讀
* 提示: `mmap` 系統呼叫
- [ ] 是否已詳閱文件 [sandbox execution environment](https://github.com/sysprog21/moxiebox/blob/master/sandbox-design.md) 呢？解釋 法國的加密貨幣硬體錢包公司 [Ledger](https://www.ledgerwallet.com/) 的 BOLOS 運作原理
- [ ] 何謂 cross compiler 呢？我們為何需要？
- [ ] ELF 執行檔格式包含哪些 section 呢？又在哪裡可見到詳細描述？
- [ ] 是否已掌握 GNU gprof 的使用？運作原理為何？
* 提示: 參閱 [raytracing](https://hackmd.io/s/HyuBWDwYl) 作業規範和共筆成果
- [ ] 是否已操作 remote GDB 呢？如何在執行時期檢驗載入的 ELF 執行檔裡頭 `.text` 和 `.data` section 內容呢？
- [ ] 是否詳讀文件 [遠端除錯](http://www.study-area.org/cyril/opentools/opentools/x1265.html) 並記錄心得呢？是否在 GNU/Linux 實際照著操作？又，遇到什麼問題呢？
* 提示: 硬體架構以不同，文章提及 IA32，但現在已是 x86_64 架構
- [ ] GDB 命令如 `step` 是如何透過 GDB stub 傳遞到 [moxiebox](https://github.com/sysprog21/moxiebox) 裡頭呢？兩邊的通訊協定又為何？
* 提示: 需要對照看 [moxiebox](https://github.com/sysprog21/moxiebox) 的 `src/sandbox.cc` 檔案內容和 [GDB Remote Serial Protocol](https://sourceware.org/gdb/onlinedocs/gdb/Remote-Protocol.html)
- [ ] 是否理解 GDB Macro 和 [Command Files](https://sourceware.org/gdb/onlinedocs/gdb/Command-Files.html) 呢？能否透過 [moxiebox](https://github.com/sysprog21/moxiebox) 進行練習呢？

---
### Model Checking
---
- [x] 自我檢查項目
- [ ] cbmc 的作用為何？在什麼領域會需要呢？
- cbmc 是一個檢查 C or C++ 程式範圍，正確的來說是在測試**陣列的範圍(buffer overflow)，指標的安全性，例外以及使用者規定還可以檢查 C and C++ 與其他語言的一致性如 Verilog**
- 好處：
- 全自動
- robust
- 比較難以找的 bugs 可以被找到
- 應用在嵌入式系統上
- [ ] 能否簡介自動機理論 (automata theory) 呢？
* 自動機理論是對抽象的機器和這些機器能解決的問題做研究助於理解。
* 有限自動機 (finite automation) 用於文字處裡 (text processing) 和 編譯器(compiler) 與硬體設計
* 與上下文無關的文法(context-free grammar)，則應用於程式設計與人工智慧上
* 參考資料：[自動機理論](http://www.wikiwand.com/zh-tw/%E8%87%AA%E5%8B%95%E6%A9%9F%E7%90%86%E8%AB%96)
* 其中談到與上下文有關及無關的解釋
* 上下文有關的：(Linear bounded automaton,LBA ) 線性有界自動機
* 上下文無關的：(Pushdown automaton,PDA) 下推狀態機，圖靈機
* 在 PDA 及圖靈機無法被判定或解決的問題，在有線狀態擊中都可以得到解答，且存在一個有效的演算法
* finite automaton 存在 5 個元素 $<Q, \Sigma, \delta, S_{0}, F>$
* $Q$ : 是狀態的集合
* $\Sigma$ : 是符號的有限集合，為自動機能接受的字母表
* $\delta$ : 代表轉換函數 $\delta:Q\times\Sigma\rightarrow Q$
* $p_{0}$ : 代表初始狀態
* $F$ : 代表可以接受的狀態集合
用以下圖解釋
- $Q = {S_1, S_2}$
- $\Sigma={0, 1}$
- $S_{1}$ 是開始狀態
- $F={S_{1}}$
- $\delta=$

||0|1|
|:---:|:---:|:---:|
|$S_{1}$|$S_{1}$|$S_{1}$|
|$S_{2}$|$S_{1}$|$S_{2}$|

- [ ] model checking 中局部狀態表示每個主題執行通訊協定的過程，而所有局部狀態構成全域狀態，每個局部狀態的改變由主體的訊息接收、發送來觸發，能否舉出實際案例說明？
- [ ] 是否已編譯 cbmc 並用來分析 C 程式呢？若是，舉出詳細的操作和你的解讀
* 務必詳閱 [CBMC: Bounded Model Checking for C/C++ and Java: A Short Tutorial](http://www.cprover.org/cprover-manual/cbmc.shtml)
* cbmc 只能編譯 .c 檔，像 linker 一樣的把功能定義與 .c 檔中的變數做結合
* cbmc 用了很大量的定義去檢視自己
* 再來是其中，在抽象定義域中去使用一個固定點去計算分析，但顯然而知的，從抽象層定義出來並不可靠，是否為正確的危險 (bug) 必須再進一步的分析
* cbmc 是使用 Symbolic simulator 去生成一個公式，使用公式與實體所有物去分析，可以用下列指令去看公式
* 指令 ： `cbmc file.c --show-vcc --bounds-check --pointer-check`
* 兩個設定：
* `--bounds-check` :
* 檢測有沒有超過 array 的界限並用 pointer 來實現
* `--pointer-check` :
* 與上面的指令共同使用，用 pointer 與 array 連合起來使用，去檢測上述的行為
* `--show-properties` : 只有呈現環境但不去 run 分析
* `--show-vcc` :
* 所以我們可以使用 `cbmc file.c --show-properties --bounds-check --pointer-check`
* 這裡我出現的錯誤跟文章裡不同 `[main.pointer_dereference.6] dereference failure: pointer outside object bounds in argv[(signed long int)2]: FAILURE` 發生在 pointer 的錯誤，所以我更改指令 `cbmc file.c --pointer-check --trace` 去找錯誤，同時我也測試`--bound-check` 去測試沒有問題
* 錯誤訊息：

這裡測試 `cbmc file.c --show-properties --bound-check --pointer-check` 及 `cbmc file.c --bound-check --pointer-check` 去分析他們的行為，發現 `show-properties` 的情況下會發生錯誤，但拿掉後不會。
~~~c=
int puts(const char *s) { }

int main(int argc, char **argv) {
if (argc >= 3)
puts(argv[2]);
}
~~~
>在這裡猜測他其中的差異為有無真正的跑程式，才會發現程式可否正確的執行

- [ ] 以 moxiebox 為例，能否使用 cbmc 來找出程式碼實作的缺陷 (或者自己創造) 呢？
- [ ] 在 GitHub 專案中找出使用 model checking 的案例，並且具體說明其作用 (當然要親自實驗)
---
### 第 6 週作業回顧
---
- [ ] 自我檢查項目
- [ ] 是否已知曉搭配 computed goto 實作更高效的 opcode dispatch 呢？舉例說明並且附上效能分析
* 運用 threaded code 的技巧，並以對應的 direct threading 解釋
- [ ] 何謂 tail recursion 呢？舉出具體而微的案例並用 perf 解釋細部差異 (特別是 cycle count 的落差)
- [ ] 是否理解 Fibonacci 數列求值的多種實作方式？若是，詳述之
- [ ] GCC 如何從 3-address code 轉換，又如何轉換出給定 ISA 的組合語言程式？
- [ ] 目前採用的 LP64 資料模型下，int 實質為 32-bit，而 $fib(46)$ 尚在 32-bit 能表示的數值範圍內，但 $fib(47)$ 該如何處理？
- [ ] Fibonacci sequence 在真實世界中究竟有何應用？
* 當然不能舉「用來刁難學生」這種案例
- [ ] Fibonacci Q-Matrix 如何運作？
- [ ] 如何設計 CPU profiler 呢？
- [ ] 如果我們也想對 full-stack-hello 提出 GDB 支援，該如何實作 GDB stub 呢？
---