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

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

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.