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.