TWC: Small: Deker: Decomposing Commodity Kernels for Verification

点击翻译按钮获取中文摘要

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.