C08: sandbox - HackMD

# 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)