TWC: Small: Deker: Decomposing Commodity Kernels for Verification

不安全的计算环境问题对社会有着巨大的影响：安全漏洞导致侵犯隐私、金融欺诈、间谍活动、破坏、生产力损失等等。这些反过来又造成了巨大的经济损失。造成这些后果严重性的一个主要原因是，许多系统运行在不安全的操作系统内核之上。Linux内核是嵌入式、移动的、云和超级计算环境的事实上的行业标准，通常是安全攻击的目标。通过提供一个安全的、经过验证的内核，该项目有可能减轻与不安全软件相关的许多最严重的问题，从而造福社会并减少经济损失。该项目将验证一个商用操作系统内核（特别是Linux）的安全性。该方法的本质是将商品内核的源代码分解为没有共享状态的独立模块，并在接口“胶水”语言Deker中表达这种分解。该方法使用一个接口语言来明确地重构内核的结果，验证任务是模块化的。除了验证和安全相关的研究，还有一种新的通信/保护机制，以提高多核计算的性能。该项目将在开放源码许可证下开发软件，并在Linux和操作系统研究社区中广泛分发和宣传。该系统将通过降低进入该领域所需的开发量，为该领域的未来研究奠定坚实的基础。最后，创新研究对于推动科学发展至关重要，需要一个多元化的研究团队。因此，计划让历来代表性不足的学生参与安全和核查领域。

The problem of insecure computing environments has large impacts on society: security breaches lead to violations of privacy, financial frauds, espionage, sabotage, lost productivity, and more. These, in turn, result in vast economic damage. A major reason for the severity of these consequences is that many systems run on top of an insecure operating system kernel. The Linux kernel, a de facto industry standard for embedded, mobile, cloud, and supercomputing environments, is often a target for security attacks. By providing a secure, verified kernel, the project has the potential to mitigate many of the worst problems associated with insecure software, thereby benefiting society and reducing economic damage. The project will verify the security of a commodity operating system kernel (in particular, linux). The essence of the approach is to factor the source code of a commodity kernel into separated modules with no shared state, and to express this decomposition in an interface "glue" language, Deker. The methodology uses an interface language to explicitly restructure the kernel with the consequence that the verification task is made modular. Aside from the verification and security related research, there is a novel communication/protection mechanism for better performance on multicore computations. The project will develop software under an open source license, and distribute and advertise it widely in the Linux and operating system research communities. The system will form a solid foundation for future research in this area by lowering the amount of development required to enter the field. Finally, innovative research, which is critical for advancing science, requires a diverse research team. Hence, the plan is to involve traditionally underrepresented students in the security and verification communities.