Many of the vulnerabilities discovered and fixed in production code arise from highly dangerous violations of memory safety; these include use-after-freesbuffer overflows, and out-of-bounds reads/writes. Despite their more than 33-year history and the many attempts aimed at mitigating or blocking their exploitation, such vulnerabilities have remained a consistent, and sometimes worsening, threat.

Internet of Things (IOT) and other special-purpose devices are also at risk. For example, a vulnerability in peer-to-peer communications services subjected millions cameras to attack 18Paul Marrapese. Abusing P2P to hack 3 million cameras. DEF CON 28 talk at, 2020.; memory-safety problems in TCP/IP stacks render millions of IOT devices at risk 2Keumars Afifi-Sabet. Weekly threat roundup: Chrome, Exchange Server, IoT devices., 2021.; and routers have had critical vulnerabilities for years 14Michael Horowitz. Router security: Router bugs flaws hacks and vulnerabilities., 2021.. In general, IOT designs are often “close to the metal,” and so developers turn to C or C++. But such developers tend not to have the experience or training of those working on browsers and operating systems, which are themselves routinely patched for memory safety problems.

On May 12, 2021, the Whitehouse released its Executive Order on Improving the Nation’s Cybersecurity 15Jr Joseph R. Biden. Executive order on improving the nation’s cybersecurity., May 2021., which sets in motion a process to develop stronger standards for assuring the security of software procured by the federal government. If successful, these standards will increase the security of all software, not just government systems. With this order in mind:

I believe that now is the time to mandate that a system with even modest security requirements provide increasingly strong evidence of its memory safety.

What forms might this evidence take? In the best case, the evidence results from some form of automated reasoning – type checkingstatic analysisformal verification – and at the least, employs automated testing.

For new development, memory safety is not hard to attain: memory safety vulnerabilities essentially occur in only C and C++ code 23Laszlo Szekeres, Mathias Payer, Tao Wei, and Dawn Song. Sok: Eternal war in memory. In Proc. of the IEEE Symposium on Security and Privacy, pages 48–62, 2013., so the requirement can be met by programming in any other programming language. In the not-so-distant past, one might have reasonably argued that for certain kinds of development, popular languages such as Java and Python are not efficient enough, and C and C++ are the only reasonable choices. But within the last ten years Google has developed Go 13Google. Go programming language., 2020.22Rob Pike. Go at Google: Language design in the service of software engineering., 2020. and Mozilla developed Rust 20Mozilla. The Rust programming language., 2020. to be practical but secure alternatives to C and C++; these languages aim to be fast, low-level, and memory-safe. Rust and Go have been rising in popularity— IEEE’s 2019 Top Programming languages list ranks them 17 and 10, respectively, and both can be used for IOT development16Fredrik Lundström. Manage security vulnerabilities in embedded IoT devices with Rust., 2019.21Poornima Narasimhan. Golang for Internet of Things — a perspective., 2019..

What about active codebases already written in C and C++? Since Rust and Go are very different languages from C and C++, legacy code could be ported, perhaps incrementally, to use language extensions such as Microsoft’s Checked C, which comprises annotations that when used pervasively will ensure spatial memory safety, ruling out out-of-bounds reads and buffer overflows 9Archibald Samuel Elliott, Andrew Ruef, Michael Hicks, and David Tarditi. Checked C: Making C safe by extension. In Proceedings of the IEEE Conference on Secure Development (SecDev), September 2018.. Microsoft is developing Checked C to be part of their Azure Sphere IOT cloud service. Checked C is open source (built on Clang/LLVM) 7Microsoft Corporation. The Checked C clang repo., 2021..

At Correct Computation, we are developing a tool, called 5C, that helps developers automatically convert legacy code to Checked C 15C: Correct Computation’s Checked C Converter., 2021..

Another approach is to use static program analysis to provide assurance that developed C code is memory safe. This is the approach being taken in FreeRTOS, a popular IOT operating system, to ensure the memory safety of its TCP library 5Nathan Chong. Ensuring the memory safety of FreeRTOS., 2020., and has been used in Amazon’s s2n TLS library 17Colm MacCarthaigh. Automated reasoning and Amazon s2n., 2016.. Static analysis differs from testing in an important way: While testing is able to uncover bugs, it is not able to prove their absence. Certain kinds of static analysis tools can do this because they are able to consider all possible program executions as part of their analysis. Even static analyzers that do not consider all executions, such as Facebook’s open-source Infer tool 10Facebook. Infer: A static analysis tool., 2021., are precise enough that they would provide helpful evidence of memory safety. Running any such tools as part of a DevOps/continuous integration (CI) process is likely to increase code security 8Dino Distefano, Manuel Fa ̈hndrich, Francesco Logozzo, and Peter W. O’Hearn. Scaling static analyses at face- book. Commun. ACM, 62(8):62–70, July 2019..

At Correct Computation, we are developing a tool, called Affix, that allows developers to run static analyzers on projects that contain binary (native) code [?].

Barring all of the above, some useful evidence of memory safety can be provided by automated reasoning- enhanced testing, such as fuzz testing and symbolic execution 3American fuzzing lop (afl)., 20214Cristian Cadar, Daniel Dunbar, and Dawson Engler. Klee: Unassisted and automatic generation of high-coverage tests for complex systems programs. In USENIX Conference on Operating Systems Design and Implementation, pages 209–224. USENIX Association, 2008.. These strategies use automated intelligence to cover more execution paths than would be covered with typical testing, thereby potentially revealing dangerous, memory safety-violating vulnerabilities. As mentioned above, testing cannot guarantee the absence of bugs, so it constitutes weaker evidence than we would like. Indeed, Chrome is regularly fuzz tested, but still suffers from memory safety bugs, as mentioned at the start.

In sum: Vulnerabilities owing to a lack of memory safety have been around far too long; they constitute a significant but addressable risk. The standard we develop should mandate evidence of memory safety. We should be flexible, at least at first, about the evidence required to prove it, but we can and should mandate that that evidence employs automated reasoning of increasing degrees.