Presented at
DEF CON China Beta (2018),
May 12, 2018, 1 p.m.
(60 minutes).
Security researchers and engineers have worked hard for decades to protect software written in memory unsafe languages like C or C++, but real world exploits show that all currently deployed protections can be defeated. Therefore, memory safe programming languages like Rust or Go get more and more attention. However, there is still a significant gap between memory safety and formal verification -- i.e. memory safety cannot guarantee that your software is vulnerability-free, and formal verification for general software is still too complex to be adopted widely.
In this talk, we propose Non-bypassable Security Paradigm (NbSP), which bridges memory safety and formal verification. The "Non-bypassable" property was introduced by MILS (Multiple Independent Levels of Security/Safety) and it requires that one component cannot use another communication path, including lower level mechanisms to bypass the security monitor. NbSP combines program analysis and specifications to ensure that critical check points are non-bypassable. In this way, NbSP reduces attack surfaces significantly, and makes it practical for either detailed manual inspection or further formal verification of authentication, authorization and auditing.
Presenters:
-
Dr. Wei (Lenx) Tao
- Chief Security Scientist at Baidu, and Adjunct Professor at Peking University
Dr. Wei (Lenx) Tao is the Chief Security Scientist at Baidu, and Adjunct Professor at Peking University. He was also a co-organizer of the BitBlaze Group in UC Berkeley. His research interest lies in security architecture, programming languages and machine learning. Beside defending Baidu against various kinds of attacks, he also initiates, directs and promotes several important open-source security projects of Baidu, such as MesaLock Linux (a memory-safe Linux distribution), Rust SGX SDK, OpenRASP, etc.
Links:
Similar Presentations: