本次系統安全暑期學校涵蓋的內容非常廣泛，有深有淺地包括了模糊測試技術，AI 系統安全，硬體輔助系統安全，傳統二進位制安全，嵌入式系統安全以及韌體分析，形式化方法等各種內容。既有對於前沿科研成果的介紹，也有技術分享的乾貨。
接下來將對幾個較為感興趣的報告作一些總結，分別是劉洋老師的有關模糊測試技術的分享，夏虞斌老師的有關硬體擴充套件的分享，以及陳立前和趙勇望老師的有關形式化技術的分享。
模糊測試技術
對於模糊測試技術，之前的瞭解較為淺顯。劉洋老師從五個方面介紹了他們小組在模糊測試方面進行的安全方面的工作。
第一部分介紹了模糊測試中如何更合理地生成種子，可以透過將上下文加入考慮，建立執行路徑的機率模型。第二部分則更細粒度地介紹瞭如何理解種子的意義，衡量種子之間的距離，以及基於優先的排序等，對之前提到的模糊測試框架的閉環有了更好的闡釋。
第三部分介紹了模糊測試如何和其他的想法進行結合。比較有啟發的一個例子是和符號執行進行結合。對於一些條件表示式（ 例如 x == 1 && y == 2） 來說，更適合使用符號執行（很快可以得到該路徑的輸入）而不是隨機 mutation ；對於另一些條件（非線性的表示式）來說，符號執行則會引入相當大的複雜度，使用隨機的演算法則更加合適。
第四部分介紹了對於特定型別的缺陷和漏洞如何進行模糊測試。用 UAF 舉例，觸發一個 UAF 必須經歷一些複雜的操作序列，因此在傳統的模糊測試中很難被觸發到。而劉洋老師的團隊將觸發 UAF 這個小目標轉化為一個有效狀態機，根據這個 FSM 的需求進行插裝，然後再在測試框架中根據這個狀態機的輸出反饋指導種子的選擇，mutation 等等，就能夠很好地對這一型別的缺陷和漏洞進行挖掘。同時，這個工作流程其實是非常通用的，能應用到很多別的目標上。
最後一個方面是模糊測試在其他領域內的使用。如何將各種概念（錯誤，mutate 等）進行領域間的遷移，也是很有趣的工作。
總體理解下來，發現劉洋老師做科研的思路非常清晰：簡單而有效的 idea ，許多研究工作給人一種「就該這樣做」的感覺，從直觀理解上和從實驗結果上看都容易被人接受。
硬體擴充套件
夏虞斌老師來自於有名的上海交通大學 IPADS 實驗室。對於硬體擴充套件方面的介紹非常的全面以及清晰，聽講座之後受益匪淺，我對於這一領域的技術發展，漏洞的基本防護思路都有了一定的瞭解。講座的結構也很清楚，首先對於用於安全增強的硬體擴充套件進行了介紹，之後是用於隔離執行環境的硬體擴充套件，最後介紹了原先並不是專用於安全增強的一些硬體擴充套件。
Intel SMEP 對資料在使用者態和核心態的執行許可權進行了限制，使得特權程式並不能直接執行使用者態可控的一些資料，因此可以減輕 Return-to-user attack 帶來的影響。類似的另一個還有 SMAP，使得特權程式不能夠直接讀寫使用者態的資料，從而核心不會解引用惡意指標。在 ARM 架構下，同樣也有類似的 PAN，PXN，UAO 等擴充套件來進行對資料在特權模式和使用者模式下訪存的限制。Intel MPX 能夠在硬體級別進行邊界檢查，但是大量的邊界檢查仍會佔用相當多的記憶體，並降低效能。Intel MPK 將記憶體進行分為 16 個域，透過使用者態的特殊指令設定 pkru 暫存器來控制域內頁的讀寫許可權。
其他一些有意思的硬體擴充套件或者概念包括：
- Intel CET，用來做 CFI，想法有兩個
- Shadow stack
- Indirect branch tracking
- SGX 中
- 用來保證記憶體完整性的 Merkel Tree 的應用挺有意思。但是大量的計算雜湊卻帶來了對於記憶體大小的限制。
- 用著
（我最喜歡的）CTR 工作模式
- 以 Huawei 手機為例的四層 Trust Level 的解釋
- Secure Domain (身份認證，eID)
- Trusted Domain (TrustZone and TEE)
- Protected Domain （Hypervisor）
- Rich Domain (Linux or Android)
- Intel MKTME( Multi-Key Total Memory Encryption)
- Intel CAT
- The 「Noisy Neighbor」 Problem，太形象了
夏老師還提到了給記憶體加 tag 的相關工作還有 PUMP（Programmable Unit for Metadata Processing），基於 Micro-Policy 從而做到更細粒度的 CFI ，Memory Protection 等。
比較有意思的點還在於，硬體擴充套件在設計之初的目的會非常單純，但是在實現之後使用它的方法可以有很多創造性的想法，從而做到一些意料之外的事情。
形式化方法
本次暑期學校共有兩個講座是有關形式化方法的，陳立前老師著重介紹了形式化方法如何在數值分析領域應用的，並提供了許多易於理解的例子來輔助學習形式化方法的基本思想和能夠做到的事情。趙勇望老師集中介紹了在安全軟體中應用形式化方法的基本思路和步驟。
陳立前老師主要從數值分析的應用場景出發，介紹了抽象解釋的基本概念，描述如何透過抽象域的演算過程來代表在具體域上面程式的執行，變數值的變化等。還介紹了最小不動點的意義和演算法，使用加寬運算元來使得計算過程快速終止的直觀解釋等等。
趙老師的講座中，可以看到形式化方法可以被理解為一種建模的工具。對於自然語言描述的規範或者是要求，可能在理解上有很多歧義。而將規範實現為具體的實現，則可能引入更多的不確定性。形式化方法引入一種規範的無歧義而同時表達能力足夠強的語言，來對各種規範進行描述。類似於數學中的描述和定義，形式化後的規範也具有了一系列性質，能夠被推導和證明出來。對於任意的軟體和實現應用形式化方法是非常不現實的，因此，現在的形式化方法只在關鍵性技術和容錯要求極高的領域中有著廣泛的應用。