Singapore Academic Cybersecurity R&D

Harnessing R&D to Secure our Nation

Securify: A Compositional Approach of Building Security Verified System  
 

• Lead PI : Thambipillai Srikanthan, Professor, NTU ( astsrikan@ntu.edu.sg )
• Host Institution : School of Computer Science and Engineering, NTU

I. Goal

Security verification and building attack-free systems are very challenging tasks in view of the size and the complexity of the IT systems, which are fast growing with the new trends of computing: cloud computing, mobile computing, cyber-physical systems, internet of things. This is mainly because a well-developed system consists of several layers in its execution stack: hardware layer, OS/micro kernel layer, library layer and program layer. Attacks in any of the layers will lead to the security breach of the system.

In this project, we aim to develop an approach that would allow us to build secure and verifiable systems ground-up, which has never been done before. First, we plan to develop an execution stack from hardware layer, OS layer to library layer (security libraries), named Securify, where each layer is formally proved to implement the specification and only the specification (to prevent the attacks like backdoor) and the system is verified to be free from vulnerabilities (to prevent advanced persistent threats (APT) and 0-Day attacks). Secondly, we will look into software security verification and secure software development. Particularly, we aim at developing a compositional approach based on Securify and develop an automatic security reasoning tool so that developers can build applications on top of Securify, use third-party untrusted components and still be able to reason about the security of the overall system.

Our vision for Securify is to enhance security on relevant areas of Singapore as a Smart City, exploring ways to integrate a secure execution stack in Autonomous Vehicles and Internet of Things devices. Our ongoing efforts with Singapore Defence (DSTA and DSO) should lead to capabilities for secure system development. Finally, we will explore opportunities for commercializing Securify as the world first verified execution stack.

II. Technologies

Security Verification

• Solve system Security from a different angle by building trust and security execution environment from scratch
• Overcome security issues by deploying composition based techniques to realize security-verified systems
• Introduce runtime verification to further improve robustness
• Serve as the secure computation entity for the large systems
• Fundational framework to enhance security on the Internet of Things.

Securify Approach Overview

Static Security Verification

A complete Security Verified execution stack from hardware, micro-kernel, libraries till programs and memory-safety code generation.

Dynamic Security Verification

• Cover security from both the execution environment itself and runtime security
• Provide runtime security in both software level and hardware level
• A compositional verification framework for reasoning of complete system security