The focus on enhancing cybersecurity through various technological approaches and methodologies, as detailed in the White House Office of the National Cyber Director’s (ONCD) document titled “Back to the Building Blocks: A Path Toward Secure and Measurable Software" underscores a pivotal shift in how organizations, especially those at the helm of technological innovation, must adapt and respond to the ever-evolving landscape of cyber threats. This document provides an overview of some strategies and technologies that are critical in bolstering cybersecurity defenses.

As developers of toolchains for memory-safe programming languages and formal verification frameworks, we find the ONCD's insights particularly relevant and compelling, especially regarding the technical building blocks mentioned in the document:

• Memory Safe Programming Languages

• Formal Methods

• Memory Safe Hardware

These are three areas in which AdaCore is and has been actively involved.

The Evolving Role of the C-suite in Cybersecurity

The document emphasizes the growing responsibilities of CIOs and CTOs to work together with the CISO to ensure cybersecurity within their organizations. The ONCD also highlights the ultimate responsibility of the CEO and board of directors in establishing cybersecurity, saying: “cybersecurity quality must also be seen as a business imperative for which the CEO and the board of directors are ultimately accountable”.

The White House thus highlights the necessity for these leaders to not only understand the technical nuances of the cyber threats facing their companies but also to actively participate in the development and enforcement of comprehensive cybersecurity strategies. This proactive approach requires a deep integration of security considerations into the business model and operational processes, thereby elevating cybersecurity from a technical challenge to a core business imperative.

AdaCore is prepared to support you in making this transition. Learn how we can help.

Embracing Memory-Safe Programming Languages: Ada and Rust

One of the White House's key recommendations is the adoption of memory-safe programming languages as a means to mitigate a significant portion of vulnerabilities that can lead to security breaches. Memory safety issues, such as buffer overflows and use-after-free errors, are common exploit vectors for attackers. By utilizing languages designed to prevent these issues, organizations can substantially reduce the risk of vulnerabilities in their software. Both Ada and Rust offer compelling options for developing secure software that is resilient against a wide array of cyber threats.

Ada, with its long history in safety-critical systems such as aviation and defense, offers a mature ecosystem for developing secure applications and employs memory safety as a key design feature. Memory safety is guaranteed in Ada through its strong type system and robust run-time checks - checks that can be safely removed if SPARK is used (see below). You can learn more about Ada memory safety features in this blog post: Memory Safety in Ada and SPARK through Language Features and Tool Support.

Rust, a more recent addition to the programming language landscape, has gained popularity for its blend of performance and memory safety guarantees. Rust offers robust memory safety without run-time checks, through its ownership model. Memory Safety in Rust

Leveraging Formal Verification Frameworks: SPARK

The ONCD also underscores the importance of formal verification frameworks. Formal verification involves mathematically proving the correctness of algorithms underlying a system, ensuring they behave as expected under all possible conditions. SPARK, a formally verifiable programming language based on Ada and toolset, enables developers to write high-assurance software, which is critically important in security-sensitive domains. By integrating formal verification into the development process, organizations can achieve a higher level of assurance that their software is free from certain types of errors or vulnerabilities.

Communications of the ACM has published a paper on SPARK: “Co-Developing Programs and Their Proof of Correctness”. The paper provides a comprehensive and up-to-date presentation of SPARK; as such, it’s a great reference to share with anyone - in industry, academia, or anywhere in between - who might like to know more about SPARK.

Advancing Security with CHERI Architecture

Another notable aspect of the document is its advocacy for the Capability Hardware Enhanced RISC Instructions (CHERI) architecture. CHERI seeks to enhance security through hardware-level innovations, offering protection against various forms of cyber attacks by implementing fine-grained memory protection and control. This architecture can significantly complement software-level security measures, providing a more robust defense mechanism against sophisticated cyber threats.

Alongside industry and UK Government partners, AdaCore is developing CHERI toolchain solutions for the Edge Avionics project. The primary goal of the Edge Avionics project is to demonstrate the ability of CHERI-related microprocessor architectures at scale on large defense platforms. AdaCore's role is to develop multiple Ada compilers for GCC, LLVM, bare-metal, and commercial-grade OSs that support a complete CHERI pure-capability Ada runtime framework. The benefits of this work bring enhanced dynamic cybersecurity solutions to the market that eradicate common security vulnerabilities triggered by software bugs like buffer overflows, null pointer access, and other forms of memory violations.

Conclusion

The ONCD report presents a multifaceted approach to cybersecurity, highlighting the critical roles of organizational leadership, advanced programming languages, formal verification, and innovative hardware architectures. As professionals at the intersection of software development and cybersecurity, we have a pivotal role to play in advocating for and implementing these technologies. By embracing memory-safe programming languages like Ada and Rust, leveraging formal verification frameworks such as SPARK, and exploring advanced security architectures like CHERI, we can contribute to a more secure digital future. This is not just a technical challenge but a strategic imperative for all organizations in the digital age. Contact us here to discuss how can AdaCore help you strengthen your building blocks.