As seasoned proponents of safety-by-design, we were pleased to see the February 26th White House press release titled "Future Software Should Be Memory Safe." The accompanying report touches on important topics, most significantly regarding the critical importance of memory safety. The U.S. government's emphasis on secure-by-design measures in software development sets a commendable example in the global cybersecurity landscape.

As experts in OCaml, a pragmatic language that combines memory safety and security by design, we encourage everyone to recognise security as a first-class software consideration. Here, we outline how OCaml fulfils the security goals presented in the report and why it is an ideal candidate for developing secure and mission-critical applications. Given Europe’s rich history of technological innovation and the EU’s commitment to digital sovereignty, wider adoption of OCaml could serve as a strategic move to strengthen cybersecurity whilst fostering the EU’s technical independence and leadership.

The Key Message

The report raises several important points with which we agree. Firstly, the focus and burden of managing existing cybersecurity threats is unreasonably placed on the user instead of the software and hardware manufacturer. The report calls for "rebalancing the responsibility to defend cyberspace to those most capable and best positioned to reduce risks for all." This means that rather than patching on fixes after the fact, the industry should aim to create solutions and products that are secure by design and safe from the start.

Secondly, the report correctly identifies that memory-safety issues are the industry's most pervasive and destructive class of vulnerabilities today. As we have previously outlined in our blog post, up to 70 per cent of zero-day attacks arise due to memory safety exploits, and the report further outlines how many of the significant cybersecurity exploits in recent time have been facilitated by memory safety vulnerabilities.

The most important conclusion, agreed upon by the report, Tarides, and numerous computer programming experts, is that your choice of programming language significantly impacts the cybersecurity of the final product.

How Does OCaml-Based Technology Address the Threats?

The report outlines the main factors affecting hardware and software security, including memory-safe programming, formal methods, software measurability and new challenges facing embedded systems in space. Let's examine these factors and whether using OCaml and OCaml-built tools can mitigate the risks.

• Memory Safety

As mentioned above, the report identifies memory safety as a critical issue. Malicious actors can take advantage of memory-unsafe languages like C and C++ to access hardware, steal data, deny access to the user and other malicious activities.

OCaml has a strong static type system and is type and memory-safe, including both spatially and temporally memory-safe. This eliminates the most pervasive and currently most destructive vulnerabilities from ever occurring in OCaml-based software. In response to the report's assertion that:

"The highest leverage method to reduce memory safety vulnerabilities is to secure one of the building blocks of cyberspace: the programming language."

We could not agree more, and OCaml is a prime example of a programming language that solves the problem that memory exploits present.

• Formal Methods and Model Checkers

The report argues that formal methods can “serve as another powerful tool to give software developers greater assurance that entire classes of vulnerabilities, even beyond memory safety bugs, are absent.”

OCaml, a language that grew out of an academic context, has several formal method tools available to the developer. Formal verification lets the developer prove the correctness of a piece of code with respect to a certain formal specification or property. Coq-of-ocaml, for example, enables programmers to use the expressive formal language Coq to verify properties in OCaml. Coq (also written in OCaml) has been used to formally verify the crypto-currency protocol Tezos, consisting of over 100,000 lines of OCaml code. Other options available for formal verification include F*, Why3, and Imandra. Most formal verification tools can export OCaml code, which is what Nitrokey uses to run formally verified cryptographic primitives for their NetHSM project.

These formal method tools can be integrated directly into the developer toolchain. The OCaml Platform provides a helpful workflow for developers to write, test, and document their code in a way that includes formal methods. For examples of formal methods in production, both Nitrokey (as mentioned above) and Tezos use formally verified OCaml components in their workflows.

Another way to apply formal methods is via model checking, and DSCheck allows OCaml programmers to test their concurrent programs and catch hard-to-reproduce bugs. In fact, OCaml Multicore has extensive tooling available for developers to test their multithreaded programs. Consequently, OCaml enables developers to incorporate formal methods in their programs and projects, ensuring more reliable and secure software solutions.

• Software Measurability

The report asserts that software measurability is one of the hardest open research problems to address, yet it is still a top priority for improving transparency, introducing useful metrics, and improving cybersecurity in the industry. Significant effort has been made to bring monitoring tools to OCaml to allow users to understand and visualise how their code is performing.

Runtime_events and Eio-trace provide OCaml developers with tools to monitor the OCaml GC and runtime (including custom user-generated events) and the I/O stack Eio, respectively for how they are behaving, including why they might be underperforming. The observability tool Olly allows users to visualise this information in ways that make it more accessible and easier to understand. It is important to provide these software measurability tools directly to all OCaml users and developers, allowing them to check their code in a transparent manner.

Furthermore, the OCaml multicore testing tools allow developers to test their multicore code to ensure it is without faults. This gives developers and users insight into how their code behaves before deployment.

• Space and Embedded Systems

We were pleased to see the report’s emphasis on secure-by-design systems for outer space, a topic we have addressed alongside Parsimoni in our SpaceOS proposal. The report states that:

First, the language must allow the code to be close to the kernel so that it can tightly interact with both software and hardware; second, the language must support determinism so the timing of the outputs is consistent; and third, the language must not have – or be able to override – the “garbage collector,” a function that automatically reclaims memory allocated by the computer program that is no longer in use.

SpaceOS easily meets the first two requirements. Firstly, thanks to MirageOS unikernel technology, which consists of specialised unikernels running under a hypervisor, SpaceOS has an extremely small footprint with code that runs directly without a kernel. Secondly, SpaceOS is written in OCaml, a deterministic language replete with security features, including memory safety, formal verification, and model checkers, just to name a few. The operating system is being incorporated into advanced satellite systems to facilitate edge computing and software-defined satellites.

Somewhat unsurprisingly, the report cautions against garbage-collected languages, of which OCaml is one. This caution is likely due to the difficulties inherent in verifying garbage collectors and the allocation problems prevalent in most garbage collectors. However, there is a way to allow OCaml’s type system and runtime to control allocation using modal types, something Jane Street has demonstrated on their blog, and recent research has shown that verified GCs are possible.

Furthermore, we disagree with the claim that garbage collectors are unsuitable for embedded systems. For embedded systems that do not require real-time guarantees, GCs are a generally accepted technology, but even in systems that do have these requirements, there is prior research to show that using a garbage-collected language works well. It is short-sighted to rule out GC languages completely since 99% of application software tolerates GC pauses. It is also important to note that using a language without a GC does not automatically mean that the hard real-time guarantees are met – the allocator may take a non-constant time to find the right-sized slot for an object allocation, for example. GC vs non-GC is a distinction without a difference for the vast majority of embedded system technologies, including systems designed for space.

• Reduced Attack Surface

Finally, we want to address an important point that was hinted at in the White House’s report and explicitly mentioned in both the CISA report report "The Case for Memory Safe Roadmaps” and the EU’s Cyber Resilience Act (CRA), which pertains to an application’s attack surface. The CRA recommends that manufacturers reduce the attack surface of their products to make it more difficult for malicious actors to exploit.

MirageOS is a technology written in OCaml that constructs specialised, fully standalone, unikernels that can run directly on bare metal or under a hypervisor. Unikernels act as individual software components, and each unikernel is standalone and responsible for one function or task. An application consists of several unikernels working together as a distributed system. As a result, MirageOS applications use up to 25 times less memory than traditional applications and have a significantly smaller attack surface than comparable virtualised solutions.

The design principles of MirageOS perfectly align with the report’s assertion that cybersecurity features should be implemented in a product or service from the start. OCaml and MirageOS projects operate on the philosophy of identifying and removing errors as early as possible, building secure solutions and applications from the ground up.

An Opportunity for Change

The White House's stance on cybersecurity begs an essential question: have we reached the time for a complete overhaul of our industry's cybersecurity strategy? We have seen multiple governments argue for change in the CISA report, and recently, the Cyber Resilience Act came one step closer to being taken into effect.

Tarides researches, develops, and implements secure-by-design software written in the functional and safe programming language OCaml. OCaml emerged from the French national research institute Inria and is now powering a large part of Wall Street exchanges and serves the network traffic of tens of millions of containers daily. Its sophisticated type system, efficient garbage collection, and emphasis on safety make it an ideal candidate for developing secure and mission-critical applications.

At Tarides, we advocate for OCaml to be part of a new strategy in the European cybersecurity sector. Globally, wider adoption of programming languages like OCaml and technologies built upon secure-by-design principles would put research-led, proven technologies first and send a clear message to the industry that the time for change has arrived.

Get in Touch

We want to hear from you! Do you have questions about this topic and what it may mean for your projects? You can contact us on our website or share your thoughts on OCaml Discuss if you want to discuss the report's implications further.

You can also stay up-to-date with us on X (formerly known as Twitter) and LinkedIN, and sign up for our newsletter to get regular updates on our projects.

Acknowledgements

We would like to thank Isabella Leandersson for her work on this article.