Try   HackMD

自我檢查項目(sandbox)

tags: 進階電腦系統理論與實作 (Fall 2017)

contributed by <jcyztw, davidshih0908>

隔離執行環境的建構

Trusted Execution Environment (TEE) 的應用為何？

可用於 DRM (Digital Rights Management，數位版權管理) 防止智慧財產權 (如 Netflix 提供的線上影片觀賞服務) 遭受侵犯。基於 Arm TrustZone 技術，一間名叫 Sansa Security (改名前為 Discretix，已於 2015 年被 Arm 收購) 的公司將其提供的硬體輔助內容保護解決方案 (hardware-assisted content protection solutions) 整合進去 Arm TrustZone ecosystem。

Sansa security 提供以下服務/產品：

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

參考資料：

Intel 的 Software Guard Extensions 關鍵特性為何？並舉出共筆以外的應用案例

根據作業中提供的參考資料，該篇文章的前三行就提到：Intel SGX 技術提供特殊的指令及軟體，可將應用程式和數據放到 enclave (被保護的記憶體區域) 中，以防被公開或是遭到修改，達到保護特定的 code 和 data 的目的。

應用案例：Numecent 使用 SGX 技術保護 DRM。

何謂 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

參考資料：

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

參考資料：

Model Checking

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

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

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

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

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

參考資料：

Last changed by 
 
Jason Chu
0
509
Published on HackMD