论文标题
Linux内核安全模块的运行时验证
Runtime Verification of Linux Kernel Security Module
论文作者
论文摘要
Linux内核是最重要的免费/Libre开源软件（Floss）项目之一。它安装在世界各地数十亿个设备上，这些设备处理各种敏感，机密或简单的私人数据。建立和证明其安全属性至关重要。该过程中的工作论文提出了一种验证Linux内核的方法，以符合Event-B规范语言中编写的抽象安全策略模型。该方法基于系统呼叫跟踪，旨在检查系统呼叫执行的结果不会导致违反安全策略要求的访问。作为它的基础，我们使用Linux系统呼叫接口的其他事件B规范，该规范被正式被证明满足了安全策略模型的所有要求。为了执行一致性检查，我们使用它来复制截取的系统调用并验证访问。
The Linux kernel is one of the most important Free/Libre Open Source Software (FLOSS) projects. It is installed on billions of devices all over the world, which process various sensitive, confidential or simply private data. It is crucial to establish and prove its security properties. This work-in-progress paper presents a method to verify the Linux kernel for conformance with an abstract security policy model written in the Event-B specification language. The method is based on system call tracing and aims at checking that the results of system call execution do not lead to accesses that violate security policy requirements. As a basis for it, we use an additional Event-B specification of the Linux system call interface that is formally proved to satisfy all the requirements of the security policy model. In order to perform the conformance checks we use it to reproduce intercepted system calls and verify accesses.
