Information Sciences Seminar——Compositional Techniques for the Verification of a Separation Micro-Kernel for Multi-Core Architectures
报告人：David Sanan (Nanyang Technological University, Singapore)
时间：2019-12-11 10:00-11:00
地点：Room 1303, Sciences Building No. 1
Abstract: The increasing presence of IoT devices and Autonomous Systems (from drones to cars) in our lives has brought significant concern regarding the security and privacy of such systems. While general operating systems like Linux and Windows fail to provide a secure environment to the applications running on them, other concepts such as the separation micro-kernel conceived by John Rushby can provide enhanced security. The complexity and concurrent architecture of this kind of kernels make possible to find exploits leading to serious vulnerabilities compromising their security.
The relative small size of the implementation of these micro-kernels make possible to apply formal verification to ensure their correctness w.r.t. functionality and a number of desired security properties. Whilst formal verification has already been conducted on micro-kernels running on single core CPU architecture, verification of multi-core CPU architectures present new challenges. In particular, it is necessary the development of new languages and the use of compositional techniques that help to cope with concurrency. In this talk I will illustrate the methodologies and techniques used for the verification of a state-of-the-art micro-kernel for multi-core architectures.
Bio: David Sanan received the M.S. degree in computer science and the Ph.D. degree in Software Engineering and Artificial Inteligent from the University of Malaga, Malaga, Spain, in 2003 and 2009, respectively. He has been working as a Research Fellow in the Singapore University of Technology and Design (SUTD), Trinity College Dublin (TCD), and National University of Singapore (NUS). In 2015 he joined Nanyang Technological University in Singapore, where he is a senior research fellow. His interest research includes formal methods, and in particular the verification of software. In the past he worked on the development of techniques for the verification of software using model checking. Currently his research topic is in the formalization and verification of separation micro-kernels aiming multi-core architectures and block-chain verification.
