Securify: A Compositional Approach of Building Security Verified System

Home / Research / Research Projects  / Securify: A Compositional Approach of Building Sec...
PI:  Thambipillai Srikanthan (NTU) Funding Source:  NRF
Co PISun Jun, Liu Yang (NTU), Alwen Tiu (NTU), Dong Jin Song (NUS), Chin Wei Ngan (NUS) Start Date:  1 January, 2015
Research Areas:  Cyber Security End Date:  31 December, 2019
Website:  -

This project aims at a comprehensive coverage of the security at each level of the execution stack. The goals include theoretical results, individual security analysis tool for each layer, and most importantly a completely verified execution stack Securify, which provides a ready platform for our collaborators to develop secure systems.

Our approach consists of building the trustworthy core Securify, secure application development and compositional verification. Firstly, we plan to develop the Securify framework as a correct and secure foundation of runtime execution. The research related to Securify has eight subprojects covering from hardware and micro-kernel verification up to program analysis and verification. At the hardware layer, we aim the verified hardware, which acts as the foundation of Securify, and dynamic security checking with hardware support. At the OS layer, Securify targets the micro-kernel verification, which runs on top of (verified) hardware, and also studies runtime security policy verification, which will be developed as part of the micro kernel. In the library layer, we will perform verification on security properties for commonly-used libraries that are needed for OS micro-kernel development. The hardware and micro-kernel layers perform functional verification of Securify. Our approach covers the complete execution stack which guarantees the security of the full system, and also delivers the Securify framework as a secure foundation for critical secure system development.