# C08: sandbox
###### tags: `sysprog2017`
:::info
主講人: [jserv](http://wiki.csie.ncku.edu.tw/User/jserv) / 課程討論區: [2017 年系統軟體課程](https://www.facebook.com/groups/system.software2017/)
:mega: 返回「[進階電腦系統理論與實作](http://wiki.csie.ncku.edu.tw/sysprog/schedule)」課程進度表
:::

## 預期目標

* 研讀 [形式化驗證](https://hackmd.io/s/H1xxp3pF0)，並透過 [cbmc](https://hackmd.io/s/Hk4lYmzkf) 做 model checking 的練習
* 探討 [隔離執行環境的建構與應用](https://hackmd.io/s/Hk9HLRbkf)，思考加密貨幣領域的系統軟體
* 深入學習 GNU Toolchain，涵蓋 GDB 和 GProf
* 延伸 [simulator](https://hackmd.io/s/BkQgqpe0Z) 作業，培養軟體設計的技巧和學習嚴謹的系統分析
* 多人協作的練習

## 隔離執行環境的建構

* 詳閱 [隔離執行環境的建構與應用](https://hackmd.io/s/Hk9HLRbkf) 並跟著練習操作
- [ ] 自我檢查項目
* Trusted Execution Environment (TEE) 的應用為何？(舉出共筆以外的真實世界案例)
* 是否已詳細閱讀 [Moxie](http://moxielogic.org/blog/) 處理器架構的 [Architecture](http://moxielogic.org/blog/pages/architecture.html) 文件？能否用 Moxie 組合語言寫出迴圈版本的 Fibonacci 數列程式？
* binutils, gcc, glibc, qemu 到 [libffi](https://sourceware.org/libffi/) 這些專案的作用為何？
* Intel 的 [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
* 詳閱 [形式化驗證](https://hackmd.io/s/H1xxp3pF0) 和 [cbmc](https://hackmd.io/s/Hk4lYmzkf)，並依據裡頭的說明，實際在 GNU/Linux 操作
- [ ] 自我檢查項目
* cbmc 的作用為何？在什麼領域會需要呢？
* 能否簡介自動機理論 (automata theory) 呢？
* model checking 中局部狀態表示每個主題執行通訊協定的過程，而所有局部狀態構成全域狀態，每個局部狀態的改變由主體的訊息接收、發送來觸發，能否舉出實際案例說明？
* 是否已編譯 cbmc 並用來分析 C 程式呢？若是，舉出詳細的操作和你的解讀
* 務必詳閱 [CBMC: Bounded Model Checking for C/C++ and Java: A Short Tutorial](http://www.cprover.org/cprover-manual/cbmc.shtml)
* 以 moxiebox 為例，能否使用 cbmc 來找出程式碼實作的缺陷 (或者自己創造) 呢？
* 在 GitHub 專案中找出使用 model checking 的案例，並且具體說明其作用 (當然要親自實驗)

## 第 6 週作業回顧

* 見賢思齊焉，見不賢而內自省也: [simulator 作業列表](https://hackmd.io/s/BJR9BTlRW)
* 詳閱並且指出具體優缺點
- [ ] 自我檢查項目
* 是否已知曉搭配 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 呢？

## 作業要求

:::info
無論完成度多高，都該在指定的共筆頁面持續有進度，並且要提供解說的錄影 (上傳到 YouTube，設定「公開」權限，好東西就要分享給大家)，在 11 月 24 日 07:00AM 前完成，以便接受教師和其他同學的檢視。
:::
* 在 GitHub 上 fork [moxiebox](https://github.com/sysprog21/moxiebox)，並設定協作者的寫入權限
* 編輯 [2017 年秋季班第一次分組表](https://hackmd.io/s/rk7xxIGkf)，新增兩個共筆頁面: (請依循給定格式，注意空白)
* ==`自我檢查事項(sandbox)`== : 答覆上述各節的「自我檢查事項」，務必詳盡回覆，誠實面對自己^TM^
* ==`開發紀錄(sandbox) / GitHub / YouTube`==: 針對下方作業要求，詳實記錄開發進度和討論，不要變成「兩個和尚沒水喝」
* 在 [moxiebox](https://github.com/sysprog21/moxiebox) 的 `tests` 目錄中，比照 [simulator](https://hackmd.io/s/BkQgqpe0Z) 作業要求，依序實作以下 Fibonacci 數列求值方法: (可用 C 程式實作，但需要附上詳盡的效能分析，善用 GNU gprof 和 GDB)
* recursive
* iterative
* Tail recursion
* Q-Matrix
* Fast doubling (加上 clz 加速)
* 善用 GNU plot 製圖和解讀
* 注意 $Fib(46)$ 之後的數值會超過 2^32^ 可表達的範圍，需要設計有效的數值表示機制來處理 (如用兩個 32-bit 暫存器保存 2^64^ 數值)
* 運用 GDB script/commands 來實作自動化測試和效能分析
* 注意: [moxiebox](https://github.com/sysprog21/moxiebox) 沒有 `printf` 可用，需要思考如何透過 `mmap` 來比對程式輸出和預期結果，自動化非常重要！
* 額外在 [moxiebox](https://github.com/sysprog21/moxiebox) 移植 (或者重新實作) 以下程式碼，並且充分驗證 (至少做一項)
1. [ctaes](https://github.com/bitcoin-core/ctaes): constant-time AES implementation
2. [constant-time-sorts](https://github.com/ktslabbie/constant-time-sorts): constant-execution-time versions of popular sorting algorithms
3. [cst_time_memcmp](https://github.com/chmike/cst_time_memcmp): onstant time memcmp() function
4. [constant_time_compare](https://github.com/levigross/constant_time_compare): constant time comparison written in C for Python 2.7
5. [CN_String](https://github.com/iDestyKK/CN_String): Stores length for constant time strlen
* 承上，詳述原始程式的演算法和應用場合，並探討在 [moxiebox](https://github.com/sysprog21/moxiebox) 移植的工作
* 務必詳閱 [dudect: dude, is my code constant time?](https://github.com/oreparaz/dudect)