自我檢查項目(sandbox)
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 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 中局部狀態表示每個主題執行通訊協定的過程,而所有局部狀態構成全域狀態,每個局部狀態的改變由主體的訊息接收、發送來觸發,能否舉出實際案例說明?
參考資料: