SaTC: CORE: Small: Practical Whole Kernel Memory Safety Enforcement

SaTC：CORE：小型：实用的整个内核内存安全实施

• 批准号: 1718997
• 负责人: Chengyu Song
• 金额: $ 47.44万
• 依托单位: University of California-Riverside
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2017
• 资助国家: 美国
• 起止时间: 2017-08-01 至 2022-07-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=1718997&HistoricalAwards=false
• 关键词: SaTC; CORE; Small; Practical; Whole

The operating system (OS) kernel is the security-critical foundation of a computer system. Unfortunately, errors in the kernel software of commodity operating systems like Windows and Linux can allow a malicious attacker to take over the whole system. This research project is developing new techniques to eliminate certain types of critical errors from commodity OS kernels in a way that is both mathematically provable and efficient.The researchers are developing a unique combination of static and dynamic techniques to provide practical spatial memory safety for commodity OS kernels. These techniques include a new type system which guarantees that for every kernel module all its memory accesses are within bounds and the corresponding access type (read, write, execute) is allowed by the module's capabilities. This is achieved by automatically inserting necessary runtime checks during compilation. Since these new checks introduce performance overhead, the project includes additional techniques to reduce the overhead. The first optimization approach is utilizing software compartmentalization and model checking to eliminate redundant checks. The second optimization is adopting Intel MPX (memory protection extension), a new and commercially available hardware feature to reduce the cost of runtime checks.

操作系统(OS)内核是计算机系统的安全关键基础。不幸的是，Windows和Linux等商用操作系统的内核软件中的错误可能会让恶意攻击者控制整个系统。该研究项目正在开发一种新的技术来消除商用OS内核中某些类型的关键错误，这种方法在数学上是可证明的，也是有效的。研究人员正在开发一种独特的静态和动态技术的组合，为商用OS内核提供实用的空间存储安全。这些技术包括一种新的类型系统，它保证每个内核模块的所有内存访问都在范围内，并且模块的能力允许相应的访问类型(读、写、执行)。这是通过在编译期间自动插入必要的运行时检查来实现的。由于这些新的检查引入了性能开销，因此该项目包括了其他技术来减少开销。第一种优化方法是利用软件划分和模型检测来消除冗余检查。第二个优化是采用Intel MPX(内存保护扩展)，这是一种新的商用硬件功能，可降低运行时检查的成本。

项目成果

Learning quantitative representation synthesis

学习定量表示综合

• DOI: 10.1145/3394450.3397467
• 发表时间: 2020
• 期刊: Proceedings of the 4th ACM SIGPLAN International Workshop on Machine Learning and Programming Languages
• 作者: Patil, Mayur;Houshmand, Farzin;Lesani, Mohsen
• 通讯作者: Lesani, Mohsen

HAMRAZ: Resilient Partitioning and Replication

• DOI: 10.1109/sp46214.2022.9833661
• 发表时间: 2022-05
• 期刊: 2022 IEEE Symposium on Security and Privacy (SP)
• 作者: Xiao Li;F. Houshmand;M. Lesani

Brief Announcement: Brokering with Hashed Timelock Contracts is NP-Hard

简短公告：使用散列时间锁合约进行经纪是 NP 难的

• DOI: 10.1145/3465084.3467952
• 发表时间: 2021
• 期刊: PODC'21: Proceedings of the 2021 ACM Symposium on Principles of Distributed Computing
• 作者: Chan, Eric;Lesani, Mohsen
• 通讯作者: Lesani, Mohsen

IAC: On the Feasibility of Utilizing Neural Signals for Access Control

• DOI: 10.1145/3274694.3274713
• 发表时间: 2018-12
• 期刊: Proceedings of the 34th Annual Computer Security Applications Conference
• 作者: M. L. Rahman;Ajaya Neupane;Chengyu Song

UBITect: a precise and scalable method to detect use-before-initialization bugs in Linux kernel

• DOI: 10.1145/3368089.3409686
• 发表时间: 2020-11
• 期刊: Proceedings of the 28th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering
• 作者: Yizhuo Zhai;Yu Hao;Hang Zhang;Daimeng Wang;Chengyu Song;Zhiyun Qian;M. Lesani;S. Krishnamurthy;Paul L. Yu