# 自我檢查項目(sandbox)
###### tags: `進階電腦系統理論與實作 (Fall 2017)`

contributed by <`jcyztw`, `davidshih0908`>

## 隔離執行環境的建構
### Trusted Execution Environment (TEE) 的應用為何？
可用於 [DRM](https://en.wikipedia.org/wiki/Digital_rights_management) (Digital Rights Management，數位版權管理) 防止智慧財產權 (如 Netflix 提供的線上影片觀賞服務) 遭受侵犯。基於 Arm TrustZone 技術，一間名叫 Sansa Security ([改名前為 Discretix](http://www.marketwired.com/press-release/discretix-technologies-ltd-announces-company-name-change-to-sansa-security-inc-1959902.htm)，[已於 2015 年被 Arm 收購](https://en.wikipedia.org/wiki/Arm_Holdings#2015)) 的公司將其提供的硬體輔助內容保護解決方案 (hardware-assisted content protection solutions) 整合進去 Arm TrustZone ecosystem。

Sansa security 提供以下服務/產品：
* DRM – Discretix 多種 DRM 用戶端方案 (支援被廣泛運用的 DRM 方案像是 Microsoft PlayReady 等)
* HDCP 和 DTCP-IP – 保護可信任裝置之間的連結
* 安全內容路徑 – 確保主要 OS 無法存取 DRM 用戶端與螢幕間的傳輸資料
* 輸出控制 – 確保高解析度影片內容僅能在核准的裝置之間共用

參考資料：
* [嵌入式技術專欄─開放式平台時代之數位版權管理 硬體輔助數位內容保護](https://www.digitimes.com.tw/iot/article.asp?cat=130&id=0000253803_tch7cjj41062dx2iz5ama)
* [Is your Android Apps Processor Ready for Premium Services?](http://www.armtechforum.com.cn/2013/3_Discretix.pdf)
* [Hardware-Assisted DRM and Link Protection from Discretix Enabling HD Video Services Worldwide](http://www.businesswire.com/news/home/20120416005489/en/Hardware-Assisted-DRM-Link-Protection-Discretix-Enabling-HD) [(中央通訊社 新聞連結)](http://www.cna.com.tw/postwrite/Detail/103024.aspx#.WhDapXWCwos "Discretix 的硬體輔助 DRM 和連結保護能達成全球的高解析度視訊服務")

---
### Intel 的 [Software Guard Extensions](https://software.intel.com/en-us/sgx) 關鍵特性為何？並舉出共筆以外的應用案例
根據作業中提供的[參考資料](https://software.intel.com/en-us/sgx "Intel Software Guard Extensions")，該篇文章的前三行就提到：Intel SGX 技術提供特殊的指令及軟體，可將應用程式和數據放到 enclave (被保護的記憶體區域) 中，以防被公開或是遭到修改，達到保護特定的 code 和 data 的目的。

應用案例：[Numecent 使用 SGX 技術保護 DRM](https://en.wikipedia.org/wiki/Software_Guard_Extensions "Wikipedia - Software Guard Extensions")。

---
### 何謂 cross compiler 呢？我們為何需要？
cross compiler 編譯出的程式可在不同於 compiler 所在的平台上執行，例如：在 Windows 7 PC 上編譯出在可在 Android smartphone 上執行的程式。

cross compiler 可用於以下情境(簡單舉例)：
* 用於資源非常有限的 target computer，舉例來說一個微波爐就是一個非常的 computer，要負責讀取觸碰板的輸入或是將輸出顯示在 digital display 上，要在這樣非常小型的 computer 編譯程式、除錯以及測試非常不容易，因此 cross compilation 比起 native compilaton 好得多。
* Bootstrapping to a new platform

參考資料：
* [Cross compiler](https://en.wikipedia.org/wiki/Cross_compiler "Wikipedia")
* [Cross Compilation Tools](https://www.airs.com/ian/configure/configure_5.html)

---
### ELF 執行檔格式包含哪些 section 呢？又在哪裡可見到詳細描述？

> TODO LIST:
> * ELF 的 sections 有何用途？
> * main() 放在哪一個 section (***hint: .symtab***)

以下列出常見的 sections：

|section名稱|說明|
|:--------:|:-:|
|.text|程式段|
|.data|資料段|
|.bss|未設初值的全域變數|
|.rodata|唯讀資料段|
|.dynamic|動態連結資訊|
|.dynstr|動態連結用字串表|
|.got|動態連結用的全域位移表|
|.plt|動態連結用的程式連結表|
|.interp|記錄程式解譯器的路徑|
|.ctors|物件導向中的建構函數|
|.dtors|物件導向中的解構函數|
|.hash|雜湊表|
|.init|在主程式執行前會執行此段落|
|.fini|在主程式執行後會執行此段落|
|.rel<name>|重定位資訊，例如： rel.text 是程式段的重定位資訊，rel.data 則是資料段的重定位資訊。|
|.shstrtab|儲存 section 名稱|
|.strtab|字串表|
|.symtab|符號表|
|.debug|除錯資訊(保留給未來用)|
|.line|除錯時的行號資訊|
|.comment|版本控制訊息|
|.note|附註資訊|

使用 `objdump` 指令可看到執行檔的詳細 sections，舉例如下：

$ objdum -x tests/basic

tests/basic：     檔案格式 elf32-little
tests/basic
系統架構：UNKNOWN!， 旗標 0x00000112：
EXEC_P, HAS_SYMS, D_PAGED
起始位址 0x00001000

Program Header:
    LOAD off    0x00000000 vaddr 0x00000f8c paddr 0x00000f8c align 2**0
         filesz 0x000004e0 memsz 0x000004e0 flags r-x
    LOAD off    0x000004e0 vaddr 0x0000156c paddr 0x0000156c align 2**0
         filesz 0x00000444 memsz 0x0000046c flags rw-

區段：
索引名稱          大小      VMA       LMA       檔案關閉  對齊
  0 .text         00000452  00001000  00001000  00000074  2**1
                  CONTENTS, ALLOC, LOAD, READONLY, CODE
  1 .init         0000000e  00001452  00001452  000004c6  2**1
                  CONTENTS, ALLOC, LOAD, READONLY, CODE
  2 .fini         00000008  00001460  00001460  000004d4  2**1
                  CONTENTS, ALLOC, LOAD, READONLY, CODE
  3 .rodata       00000004  00001468  00001468  000004dc  2**2
                  CONTENTS, ALLOC, LOAD, READONLY, DATA
  4 .data         00000430  0000156c  0000156c  000004e0  2**2
                  CONTENTS, ALLOC, LOAD, DATA
  5 .eh_frame     00000004  0000199c  0000199c  00000910  2**2
                  CONTENTS, ALLOC, LOAD, DATA
  6 .ctors        00000008  000019a0  000019a0  00000914  2**2
                  CONTENTS, ALLOC, LOAD, DATA
  7 .dtors        00000008  000019a8  000019a8  0000091c  2**2
                  CONTENTS, ALLOC, LOAD, DATA
  8 .bss          00000028  000019b0  000019b0  00000924  2**2
                  ALLOC
  9 .comment      0000003b  00000000  00000000  00000924  2**0
                  CONTENTS, READONLY
 10 .debug_aranges 000000f0  00000000  00000000  0000095f  2**0
                  CONTENTS, READONLY, DEBUGGING
 11 .debug_info   000031bb  00000000  00000000  00000a4f  2**0
                  CONTENTS, READONLY, DEBUGGING
 12 .debug_abbrev 00000cbe  00000000  00000000  00003c0a  2**0
                  CONTENTS, READONLY, DEBUGGING
 13 .debug_line   00000d8f  00000000  00000000  000048c8  2**0
                  CONTENTS, READONLY, DEBUGGING
 14 .debug_frame  00000178  00000000  00000000  00005658  2**2
                  CONTENTS, READONLY, DEBUGGING
 15 .debug_str    00000a12  00000000  00000000  000057d0  2**0
                  CONTENTS, READONLY, DEBUGGING
 16 .debug_loc    00000415  00000000  00000000  000061e2  2**0
                  CONTENTS, READONLY, DEBUGGING
 17 .debug_ranges 00000038  00000000  00000000  000065f7  2**0
                  CONTENTS, READONLY, DEBUGGING

參考資料：
* 巨人的肩膀(同學共筆)：[Team 2 (zhanyangch, tina0405, LinRiver)](https://hackmd.io/s/HJP5QDOJf)
* [目的檔格式 (ELF)](http://sp1.wikidot.com/elfobjfile)

---

## Model Checking

### cbmc 的作用為何？在什麼領域會需要呢？

對於 `array` 邊界問題（存取是否越界），`pointer safety` (ex:假設 `pointer` 原本指向一個 `array` 的起始，假如想對 `pointer ` 去做運算，應該保持有另一個 `pointer` 指向該 `array` 的起始 or 尾巴)，`exceptions`等等，確保其不會發生。依[CBMC](http://www.cprover.org/cbmc/)所敘述，主要應用領域為 `embedded system` 。但我覺得只要是以 `CBMC` 所支持的程式語言寫成的程式都可以依其去測試。

---

### 能否簡介自動機理論 (automata theory) 呢？

數學家為了想更了解機器是如何去解決問題，而且此問題是有確定的答案的。進而提出了一個數學模型，將輸入資料透過狀態的不斷轉移、運算，並得出一個輸出結果。

### model checking 中局部狀態表示每個主題執行通訊協定的過程，而所有局部狀態構成全域狀態，每個局部狀態的改變由主體的訊息接收、發送來觸發，能否舉出實際案例說明？

---

參考資料：
* [CBMC](http://www.cprover.org/cbmc/)
* [CBMC: Bounded Model Checking for C/C++ and Java ](http://www.cprover.org/cprover-manual/cbmc.shtml)
* [Automata Theory](https://cs.stanford.edu/people/eroberts/courses/soco/projects/2004-05/automata-theory/basics.html)