AdaCore Shows How to Address the Cybersecurity Challenge

Free book offers guidance for achieving secure and reliable software 

 PARIS & NEW YORK & GAITHERSBURG, Maryland, June 27, 2018 – Workshop on Sound Static Analysis for Security - AdaCore, a trusted provider of software development and verification tools, today announced the availability of AdaCore Technologies for Cybersecurity, the latest volume in its series of free publications on high-assurance software. Authored by internationally known experts Dr. Roderick Chapman and Dr. Yannick Moy, the book explains why making a cyber system secure is so difficult and shows how using appropriate programming languages and tools can contribute to a solution. Languages such as Ada and SPARK, and verification based on formal methods or other sound static analysis techniques, can prevent vulnerabilities from being introduced in the first place. They can also detect latent issues in legacy codebases, including many of the weaknesses in the MITRE Corporation’s Common Weakness Enumeration (CWE).

“Many of the nasty security-related incidents that we’ve seen over the past few years stemmed from entirely preventable software errors,” said co-author Yannick Moy, a senior software engineer at AdaCore. “By following the guidance presented in our new book, software developers can learn from history and avoid repeating it.”

“Developing software that is robust in the face of malicious attack is a huge engineering challenge,” said co-author Roderick Chapman. “It requires a world-class combination of languages, technologies, disciplines and skills. Ada, SPARK, and AdaCore’s tools can provide some key pieces of that puzzle. In particular, AdaCore has pioneered the development of static verification techniques that are both formal and sound, and so offer real assurance. I hope the book will inform, entertain, and challenge readers’ preconceptions about how high-assurance software can be developed and verified.”

AdaCore Technologies for Cybersecurity contains four principal chapters.

·      The Challenge of Secure Softwareidentifies the various factors that make security so hard to achieve, ranging from the interconnected nature of modern systems to the limits of testing as a verification mechanism.  The chapter concludes with “A Manifesto for Secure Software” that outlines the basic principles for high-integrity software engineering.

·      Languages, Tools and Technologies Overviewsummarizes the Ada and SPARK languages, as well as AdaCore’s tools and technologies, and highlights their contributions to system security.

·      Security Vulnerabilities and Their Mitigationconsiders a number of specific high-profile software vulnerabilities, inspired by the CWE/SANS “Top 25 Most Dangerous Software Errors”, and discusses how each can be prevented or mitigated using Ada, SPARK, and AdaCore’s tools.

·      Industrial Scenario Examplespresents a number of security-related scenarios that may arise in real-world projects. Each opens with a description of the context and the security issue, and then shows how either Ada or SPARK, in conjunction with the relevant AdaCore tools, can contribute. Each scenario is illustrated with one or more examples drawn from experience with customers and industrial projects.

Complementing the discussion in these chapters, additional details and examples are provided in two appendices. One appendix focuses on the MITRE Corporation’s Common Weakness Enumeration (CWE) and shows how the use of Ada and/or SPARK, as well as AdaCore’s tools, can address specific CWEs. The second appendix shows how contract-based programming in SPARK or Ada, verified by the corresponding static or dynamic analysis, can help avoid the “SQL Injection” vulnerability.

AdaCore Technologies for Cybersecurityis available at adacore.com/cyber-security-book; to request a printed copy, please contact info@adacore.com.

About AdaCore

Founded in 1994, AdaCore supplies software development and verification tools for mission-critical, safety-critical and security-critical systems. Four flagship products highlight the company’s offerings:

·      The GNAT Pro development environments for Ada, C and C++, comprising complete toolsets for designing, implementing, and managing applications that demand high reliability and maintainability,

·      The CodePeer advanced static analysis tool, an automatic Ada code reviewer and validator that can detect and eliminate errors both during development and retrospectively on existing software,

·      The SPARK Pro verification environment, a toolset based on the formally analyzable SPARK Ada subset (co-developed by AdaCore and Altran) and oriented toward high-assurance systems, and

·      The QGen model-based development tool suite for safety-critical control systems, providing a qualifiable and customizable code generator and static verifier for Simulink^®and Stateflow^®models, and a model-level debugger.

Over the years customers have used AdaCore products to field and maintain a wide range of critical applications in domains such as commercial avionics, automotive, railway, space, military systems, air traffic management/control, medical devices and financial services. AdaCore has an extensive and growing worldwide customer base; see www.adacore.com/industries/ for further information.

AdaCore products are open source and come with expert online support provided by the developers themselves. The company has North American headquarters in New York and European headquarters in Paris. www.adacore.com/

Press Contacts