At AdaCore we pledge to timely analyze vulnerabilities in our products and disclose them in a way that balances the interests of our customers & community.
GNAT Pro for CHERI enhances memory safety in modern systems and eradicates many memory-related vulnerabilities. It also provides a complete Ada toolchain to build secure applications executing on Arm Morello, a Capability Hardware Enhanced RISC Instructions (CHERI) CPU. Enhancements to the GNAT Pro GCC and LLVM bare-metal Ada runtimes bring automated CHERI pure-capability memory allocators and other novel security features to the developer, permitting new security-by-design paradigms to systems development.
Building secure software is a challenging task. It seems that almost every
week we read the news about yet another computer system that has
failed in some way in the face of malicious or accidental misuse. “Cyber
Security” is a wide-ranging field, spanning human factors, hardware
design, sociology, and legal issues, in addition to software engineering.
This booklet summarizes the contribution that the Ada and SPARK
languages and AdaCore’s tools can make to this final area—how to
develop and verify correct and secure software.
Unlike AdaCore’s previous guides to airborne and rail system software,
this booklet does not follow the structure or requirements of a particular
standard—in part because there is no widely used security standard that
is required in practice. Instead it offers a more general treatment of the
problem, but also includes an analysis of how AdaCore’s technologies
help address the weaknesses identified in the MITRE Corporation’s
Common Weakness Enumeration (CWE). The content is based on the
authors’ many years of practical experience in the development of
high-end secure systems, the design of the Ada and SPARK programming
languages, and research into program verification tools.
The booklet is intended for readers who are involved with software at
any level (developers, project managers, procurement personnel) and
who would like to learn how currently available technology can help
address some of the most serious challenges associated with software and
security. Our goal is to provide useful guidance both to those who are
using other languages and are interested in the benefits that Ada offers,
and to existing Ada users who might be confronted with new security
requirements.
When safety-critical software malfunctions people lives are in danger. When security-critical software is cracked national security or economic activity may be at risk. As more and more software embraces object-oriented programming (OOP) safety-critical and security-critical projects feel compelled to use object-orientation. But what are the guarantees of OOP in terms of safety and security? Are the design goals of OOP aligned with those of safe and secure software (S3) systems? In the following sections we look at key OOP aspects and analyze some of the hazards they introduce with respect to S3 and outline a possible way of addressing these vulnerabilities. Specifically, after a quick overview of OOP in section 2, section 3 deals with inheritance and shows some of its hazards in terms of S3 along with possible remedies. Section 4 focuses on dynamic binding and suggests a safer and more secure implementation than what is conventionally done. Finally, section 5 looks at testing programs with dynamic binding.
In an age where security breaches and cyberattacks have become increasingly prevalent,
the need for robust and comprehensive security mechanisms within embedded real-
time systems is paramount. In this paper, we propose a novel solution to enforce fault-detection
and increase security assurance: “Security by Default”, specifically combining Capability
Hardware Enhanced RISC Instructions (CHERI) ISA microprocessor extensions with a CHERI
pure-capability compliant Ada runtime. We present case studies showing how combining
memory-safe hardware with memory-safe software results in a mutualistic layered
approach to security and increases assurance of embedded real-time systems. We argue
that this satisfies regulatory security verification objectives outlined in standards like the
“Airworthiness Security Process Specification” (DO-326A/ED-202A[1] [2]).
When it comes to providing software assurance, SPARK, a formally provable subset of Ada, is the best weapon in the arsenal to ensure the absence of data-flow and runtime errors. Furthermore, SPARK offers mechanisms to prove key integrity properties and even complete functional proof of requirements. Regardless of the apparent benefits of using SPARK in safety-critical applications, there is still some reservation in adopting the technology over traditional languages like C and C++, which offer minimum software assurance. Instead, developers in many cases rely on heavy testing approaches with the hope that all the possible bugs will be captured before application deployment. Arguments in favour of such problematic approaches include a perceived steep-learning curve for adopting SPARK, and thus, an increase in production cost, and the assumption that SPARK will significantly negatively impact the execution time of an application. These are all perceptions mainly formed due to a lack of understanding the technology. This paper takes a quantitative approach, where SPARK is put under test, and relevant metrics, such as performance and development time, are recorded to demystify the impact of adopting SPARK and expose any areas that the technology can be further improved. To achieve this a relevant to the industry embedded benchmark suite written in C, the EMBENCH, is converted to Ada and SPARK, to prove the absence of runtime errors, which are well-known sources of security vulnerabilities. Furthermore, we share our valuable experiences on best practices for hardening software libraries using SPARK.
Written by Kyriakos Georgiou, Paul Butcher and Yannick Moy
Sound Static Analysis for Security: this two-day workshop is focused on decreasing software security vulnerabilities. Sign up today to attend the event.
Sound Static Analysis for Security: this two-day workshop is focused on decreasing software security vulnerabilities by orders of magnitude, using the strong guarantees that only sound static analysis can provide. The workshop is aimed at developers, managers and evaluators of security-critical projects, as well as researchers in cybersecurity.
NEW YORK, January 22, 2007 – AdaCore, the leading Ada technology supplier, today announced the appointment of Gregory A. Gicca as the Director of Safety and Security Product Marketing. In this role Mr. Gicca will help plan, guide, and promote AdaCore’s GNAT Pro product offerings for the safety-critical and high-security sectors.
Julien Signoles is one of the main developers of Frama-C, a code analysis framework for C code, and the author of E-ACSL, its runtime verification plug-in.
This report offers further guidelines and considerations to the security refutation objectives described within the following two technically identical documents:
ED-203A “Airworthiness Security Methods and Considerations”, European Organisation for Civil Aviation Equipment (EUROCAE)
DO-356A “Airworthiness Security Methods and Considerations”, Radio Technical Commission for Aeronautics (RTCA)
Refutation is described within ED-203A / DO-356A as follows:
“Refutation acts as an independent set of assurance activities beyond analysis and requirements. As an alternative to exhaustive testing, refutation can be used to provide evidence that an unwanted behavior has been precluded to an acceptable level of confidence. NOTE: Refutation is also known as Security Evaluation in some contexts.” [ taken from ED-203A / DO-356A].
The main part of the report summarizes how refutation activities fit into the associated Airworthiness Security Process. In addition, a series of guidelines and considerations for including a Refutation Test Plan within a Plan for Security Aspects of Certification (PSecAC) is presented. Annexes are then provided to cover additional guidelines for specific refutation activities. This version of the report includes Annex A, which covers “Fuzz Testing”.
The Digital Security by Design (DSbD) programme from UK Research and Innovation (UKRI) is transforming digital technology and creating a more resilient, and secure foundation for a safer future. Across the current DSbD ecosystem, industry and academia are discovering the benefits of porting and refactoring their code to the Morello prototype platform. AdaCore are involved in the initiative via the GE Aerospace primed Edge Avionics project
In an age of increasing security breaches and cyberattacks, the need for robust and comprehensive security mechanisms within embedded real-time systems is paramount.
NEW YORK and PARIS, August 23, 2010 – With each new model year, cars are becoming more dependent on microprocessors and complex software, challenging the auto industry to ensure that these systems are secure, safe, and reliable. According to AdaCore, this challenge is not being met: security and safety issues are not being properly considered at the start of the automotive system design cycle, but are instead being addressed as an afterthought. A recent paper from Rutgers University and the University of South Carolina, detailing preventable security flaws of in-car wireless networks, confirms AdaCore’s thesis.
Let's get started…Input validation consists of checking a set of properties on the input which guarantee it is well-formed. This usually involves excluding a set of ill-formed inputs (black-list) or matching the input against an exhaustive set of well-formed patterns (white-list).
Let's get started…The notions of tainted data and trusted data usually refer to data coming from the user vs. data coming from the application. Tainting is viral, in that any result of a computation where one of the operands is tainted becomes tainted too.
The conference will focus on cyber safety for embedded systems (ie. the confluence of safety and security), and how innovations in testing and the application of formal methods can help to achieve those objectives. Talks will address themes including the state of the art in software testing, using fuzz testing in a civil avionics security certification context (DO-326A), and applying innovative techniques such as formal methods to achieve cybersecurity.
This year, the conference will feature a keynote talk about the work of the National Cybersecurity Centre in the domain of embedded and critical systems.
This webcast will discuss how to select the optimal development tools and processes to ensure the safety, security, and reliability of real-time unmanned aircraft, onboard software, and ground control solutions.
NORTHPORT AND NEW YORK, N.Y. – June 26, 2019 – Code Dx, Inc., provider of an award-winning application security management solution that automates and accelerates the discovery, prioritization, and risk management of software vulnerabilities, today announced its partnership with AdaCore, a trusted provider of software development and verification tools for the Ada, C, and C++ programming languages.
The challenges faced by companies like your own in confronting increasingly hostile cybersecurity environments and how NVIDIA is tackling this to overcome a scarcity in expert software security resources
Learn why NVIDIA made the “heretical” decision to abandon C/C++ and adopt SPARK as its coding language of choice for security-critical software and firmware components and the impact this had
The advantages of using the SPARK for security- and safety-critical coding applications
How NVIDIA's tried and tested approach to ramping up their use of SPARK for critical component development can help your business
The benefits NVIDIA has gained through their adoption of SPARK
Why many of NVIDIA’s early SPARK skeptics have now become SPARK evangelists
NVIDIA’s recommendations for would-be SPARK adopters
See first-hand how you can adopt SPARK to establish and demonstrate assurance against cyberattacks and critical system failures
As one of the world's most trusted names in high-performance computing, security is essential to NVIDIA’s brand. With cybersecurity risks rising across the board, the company took an ambitious path to examine its software development methodology and find a more measurable solution. Ultimately, it chose to abandon C/C++ and adopt SPARK as its coding language of choice for verifying its most security-critical software and firmware components.
NEW YORK, PARIS, and CEDAR RAPIDS, Iowa, September 17, 2012 - Design East Boston 2012 - AdaCore today announced the successful usage of its SPARK Pro and GNAT Pro High-Security products by Rockwell Collins in the development of the SecureOne™ Guard, a high assurance cross domain guard for military tactical systems. The SecureOne Guard has strict requirements for reliability and security. In order to meet these needs, Rockwell Collins selected SPARK Pro and GNAT Pro High-Security as key development tools for the project.
AdaCore, which provides software development tools for mission-critical systems, and embedded software security company CodeSecure, today announced a definitive merger agreement. The merger creates a unified company committed to advancing software safety, security, and reliability across critical industries.
The Sound Static Analysis for Security Workshop will be held at NIST in Gaithersburg, MD. Accommodations and transport are available at the Holiday Inn
Dr. Wheeler will provide an overview of how sound static analysis approaches can facilitate the development of higher quality and more secure software.
Dr. K. Rustan M Leino is a Senior Principal Engineer at Amazon. He is known for his work on formal techniques and tools for verifying software correctness.
Laurent Voisin has been applying formal methods in industry for 20 years. He has gained experience in using formal methods in actual development projects.
Claire has a PhD in computer science specialized in formal proof of programs. She has been working as a software developer and proof expert at AdaCore.
David Cok is a researcher in formal methods and deductive verification, with an emphasis on practical application to industrial software. See his talk.
Rod is working on merging the discipline of traditional high-integrity processes with agile approaches and the philosophy of the Lean Engineering Movement.
David Mentré focuses his research on Formal Methods as a way to ensure 100% correctness of crucial properties in safety critical systems at a lower cost.
Joe Kiniry will focus on opportunities and challenges in using several Frama-C plugins as compared to comparable tools for other platforms and languages.
AdaCore Technologies for Cybersecurity AvailableCodePeer Support for the Common Weakness EnumerationSmaller and More Secure with SPARKAdaCore Training ServicesWorkshop on Sound Static Analysis for SecurityNew Platform SupportAdaCore BlogsInterview with Emma AdbyTech Days 2018Put Some SPARK in Your Ada
The CodePeer Static Analysis tool may be used with any standard Ada compiler, scans for numerous CWE software errors, and supports all versions of Ada.
GNAT Pro Assurance offers developers the chance to freeze on a stable version of the GNAT technology - essential for long-lived projects or certification.
GNATtest (based on AUnit) helps automate processes for developing and managing the large number of test cases needed for verifying large software systems.
No-cost toolset (binary distribution of the GNAT toolset, add-ons and libraries) and support designed to give educators the tools they need to teach Ada.
AdaCore provides targeted tools and services to customers in industries with a need for safety and security. Learn more about our industries and customers.
12 September 2017 AdaCore and Altran have announced their renewed sponsorship of the annual High Integrity Software Conference, which takes place in Bristol on 17th October 2017. Now in its fourth year, the mission of the High Integrity Software Conference is to share challenges, best practice and experiences between software engineering practitioners engaged in complex systems. The conference is endorsed by official supporters BAE Systems and Jaguar Land Rover and plays host to a number of industrial exhibitors.
20 September 2016 — AdaCore and Altran have announced their renewed sponsorship of the annual High Integrity Software Conference, which takes place in Bristol on 1 November 2016.
Commemorating Lady Ada’s 200th birthday, AdaCore’s detailed graphic summarizes her life and accomplishments, recaps milestones and resources for programming language named in her honor
NEW YORK and PARIS, July 2, 2015. With great sadness, AdaCore announces the passing of Robert Dewar, company President and one of its founders. Dr. Dewar succumbed to cancer on June 30, 2015. He had a distinguished career as a Professor of Computer Science at New York University (NYU), played a key role in the design and implementation of the Ada programming language, and founded AdaCore, along with four colleagues, in 1994. He served as its CEO until 2012 and as its President until his death.
Advanced static analysis tool for Ada has been qualified under DO-178B and EN50128, adds support for IEEE 754 floating point semantics and enhances support for project files
New tool helps Ada developers keep technical debt in check, supports quality assurance activities, integrates and aggregates results of AdaCore’s static and dynamic analysis tools
Automatic code review and validation tool meets rigorous industry software verification standards; provides trusted reliability for Ada developers in safety-critical applicationsNEW YORK, PARIS and BRISTOL, October 23, 2014, High Integrity Software Conference, Bristol, UK -- AdaCore today announced that its CodePeer advanced static analysis tool for the automated review and validation of Ada source code has been qualified as a software verification tool for developers in both avionics and railway industries.CodePeer assesses the program before execution to find errors efficiently and early in the development life cycle. Using advanced mathematics, CodePeer analyzes every line of software, considering every possible input and every path through the program. It performs impact and vulnerability analysis when existing code is modified, and, using control-flow, data-flow and other advanced static analysis techniques, it detects problems that would otherwise require labor-intensive debugging.“In safety-critical domains, developers need very strong assurances that the tool they’re using to assess their code is reliable, can be trusted, and will substantially reduce the need for manual code review,” says Arnaud Charlet, CodePeer Product Manager and Technical Director at AdaCore. “CodePeer has been through rigorous industry-specific tests for avionics and railway that fully affirm its value and reliability in these and other safety-critical development environments.”
NEW YORK, PARIS and BRISTOL, October 23, 2014, High Integrity Software Conference, Bristol, UK – AdaCore today announced that its GNAT Pro cross-development environment has been selected by the Polytechnic University of Madrid (Universidad Politécnica de Madrid / UPM), for the UPMSat-2 UNION satellite project’s real-time on-board and ground control software. The 50kg micro-satellite, scheduled to be launched in Q4 2015, will provide a technology demonstration platform for the university from a sun-synchronous orbit nearly 600 km above Earth.
NEW YORK and PARIS, September 25, 2013 – AdaCore today launched AdaCore University - a free, web-based resource center for anyone interested in learning about, or how to program in, the Ada programming language. The new website offers pre-recorded courses and other learning materials on Ada, with access to AdaCore’s GNAT Ada toolset for writing and running example programs. It also utilizes the latest in website design and learning tool features. Students at all levels of experience and expertise can begin writing programs quickly and can proceed at their own pace.
SAN JOSE, Calif., NEW YORK and PARIS, April 23, 2013 – Design West Conference – AdaCore and Altran today announced TOYOTA InfoTechnology Center (ITC) Japan’s selection of the SPARK language and SPARK Pro toolset for a high-reliability software research project. The goal of the project is to show that software requirements can be transformed into an implementation that can be proven to be free of run-time errors. This will have the key advantage of providing ultra-low-defect software for higher reliability in a vehicle component. An added benefit is the reduction of development and maintenance effort, since the formal approach being used can give mathematical assurance to a variety of correctness properties, reducing the need for certain types of testing and eliminating the need for post-deployment corrections.
SAN JOSE, Calif., NEW YORK and PARIS, April 23, 2013 – Design West Conference – AdaCore today announced the release of CodePeer 2.2, the advanced static analysis tool that helps developers detect potential run-time and logic errors in Ada programs. CodePeer is able to find non-trivial problems by systematically analyzing every possible input and path through the program, and can be employed very early in the development cycle to identify defects when they are the least costly to repair.
PARIS, NEW YORK, December 17, 2012 – Paris Space Week 2012- AdaCore today announced that Terma A/S has selected the GNAT Pro Safety-Critical development environment to develop onboard software for the Atmosphere-Space Interactions Monitor (ASIM) that will be mounted on the Columbus module of the International Space Station. Terma will useGNAT Pro Safety-Critical combined with the GNATemulator and GNATcoverage dynamic testing tools to develop and test the application prior to deployment on the actual LEON 3 embedded processor.
BOSTON, December 4, 2012 - ACM SIGAda HILT Conference - AdaCore today announced the successful usage of its Code Traceability Analysis for DO-178B by Rockwell Collins in the certification of the Integrated Display System (IDS) for a large, next-generation, commercial aircraft. The Traceability Analysis package is part of the evidence needed to satisfy the DO-178B objectives for structural code coverage at Level A, the highest (most stringent) level for avionics software safety.
PARIS, NEW YORK, June 20, 2012 - SG PARIS 2012 Conference - AdaCore today announced that SmartSide, a Paris-based company providing Smart Metering and Smart Grid management solutions, has adopted the Ada programming language and AdaCore’s GNAT Pro development environment for the implementation of their Smart Devices platform. SmartSide offers multi-energy meter data management systems. Distribution Network Operators use SmartSide technology to optimize their Smart Grid networks through the secure, reliable, highly-interoperable and business-oriented Smart Energy Core platform.
PARIS, NEW YORK, and GÖTEBORG. June 12th, 2012 – Ada Europe Conference - AdaCore today announced that Saab Electronic Defence Systems (Sweden) has adopted the CodePeer static analyzer tool for use on the GIRAFFE project. This advanced static analysis tool helps developers detect potential run-time and logic errors in Ada programs. By mathematically analyzing every line of software, and considering every possible input and every path through the program, CodePeer can be used very early in the development lifecycle to identify problems when defects are much less costly to correct.
SAN JOSE, Calif., NEW YORK and PARIS, March 26, 2012 – Design West Conference – AdaCore, provider of tools and expertise for the mission-critical, safety-critical, and security-critical software communities, today announced that Embraer Defense and Security has selected the GNAT Pro Ada development environment from AdaCore as a primary tool set to develop the Operation Flight Program for the AMX Modernization program. GNAT Pro will be used along with Wind River’s VxWorks real-time operating system (RTOS) as the foundation to develop this critical software system on the AMX Modernization effort.
NEW YORK, PARIS and TOULOUSE, France, November 29, 2011 - Certification Together Conference – AdaCore, provider of Ada tools and expertise for the mission-critical, safety-critical, and security-critical software communities, today announced that Eurocopter has chosen the GNAT Pro High-Integrity Edition for development of an ARINC-653 demonstrator for military helicopters. The demonstrator will provide military interfaces and operational functions within a time- and memory-partitioned ARINC-653 architecture.
NEW YORK, PARIS and NUREMBURG, Germany, March 1, 2011 – Embedded World Conference - AdaCore, provider of tools and expertise for the mission-critical, safety-critical, and security-critical software communities, today announced that Airbus Military has successfully certified the Airbus Military Aerial Refueling Boom System (ARBS) on the A330 Multi Role Tanker Transport (MRTT). The certification was simplified by the use of the qualified GNATcheck tool to verify conformance to the software coding standard required by the ARBS project. Verification of conformance was undertaken as part of the DO-178B level A Software Verification Process.
AdaCore Releases First Non-Intrusive Coverage Tool to Fully Support All Levels of Safety CertificationNew GNATcoverage tool provides advanced program coverage analysis on both object code and source code
NEW YORK and PARIS, September 21, 2010 – Embedded Systems Conference BostonAdaCore, a leading supplier of Ada development tools and support services, today announced a comprehensive set of tools and support services for projects where Ada is used in conjunction with other programming languages. Available with GNAT Pro 6.3, the latest release of AdaCore’s Ada Development Environment, the solutions include tools and libraries to handle the various ways in which multi-language systems are designed and constructed.
AMSTERDAM, NEW YORK and PARIS, March 24, 2010 – Avionics Europe 2010 – AdaCore today announced that global display company Barco has developed an advanced business jet avionics display system using the AdaCore GNAT Pro Ada development environment. Barco selected the GNAT Pro High Integrity Edition, along with the Traceability Kit, running on Wind River’s VxWorks 653 RTOS in order to meet the highest levels of safety standard DO-178B.
New York and Newcastle, United Kingdom, September 22, 2008 – SAFECOMP 2008 - AdaCore, provider of the highest quality Ada tools and support, today welcomed the 150th member to the GNAT Academic Program (GAP), demonstrating the success of the company’s grass-roots initiative created to help bring Ada to the forefront of university study.
NEW YORK and PARIS – September 9, 2008 – AdaCore, provider of the highest quality Ada tools and support, today announced the appointment of Ada expert Stephen Baird to the company’s GNAT Pro implementation team. In this role, he will participate in the development and enhancement of the GNAT Pro technology, and provide expert support for AdaCore customers.
NEW YORK, AMSTERDAM, Netherlands, and BANGALORE, India, March 5, 2008 – Avionics 2008 - AdaCore, provider of the highest quality Ada tools and support services, today announced that the Indian Aeronautical Development Establishment (ADE) has chosen AdaCore’s GNAT Pro High-Integrity Edition for DO-178B Ada environment to be used by AdaCore’s partner Mistral Solutions to create new safety-critical flight control systems that will underpin advanced Indian defense programs.
TOULOUSE, France and NEW YORK - January 30, 2008 – Embedded Real-time Software (ERTS) Conference - AdaCore, provider of the highest quality Ada tools and support services, today announced the availability of GNATcheck, an integrated coding standard verification tool within the GNAT Pro development environment. GNATcheck meets the growing need for automated verification in safety-critical avionics systems, particularly those systems that need to satisfy the DO-178B standard. Developed by RTCA and EUROCAE, DO-178B defines the guidelines for development of aviation software in both the US and Europe and is being increasingly adopted by other related sectors, such as air traffic control and military applications.
FAIRFAX, Va., November 6, 2007 - SIGAda 2007 - AdaCore, provider of the highest quality Ada tools and support services, today announced the upcoming release of GNAT Programming Studio (GPS) 4.2. This Ada-oriented IDE (Integrated Development Environment) accompanies AdaCore’s GNAT Pro toolset on most platforms.
FAIRFAX, Va., November 6, 2007 - SIGAda 2007 - AdaCore, provider of the highest quality Ada tools and support services, today announced that Raytheon has delivered the Ship Self-Defense System (SSDS) Mk 2 using GNAT Pro for LynxOS within its multi-language software development environment. SSDS Mk 2 is a combat system that integrates and coordinates the sensors and weapons systems aboard a US Naval vessel to provide a coherent tactical picture for situational awareness, command and controls, and quick-reaction self-defense. It is a single-source baseline that supports multiple system configuration modifications (MODs) for large deck ship classes (aircraft carriers and amphibious ships). GNAT Pro was specifically used on the SSDS Mk 2 to support Ada application development on the Intel processors and the LynxOS operating system.
PARIS and NEW YORK, October 29, 2007 - AdaCore, provider of the highest-quality Ada tools and support services, today announced its participation as a member of the TOPCASED Project (Toolkit in Open Source for Critical Applications & System Development).
BOSTON, Mass. – September 18, 2007 – Embedded Systems Conference - AdaCore, provider of the highest quality Ada tools and support services, today announced another successful deployment of a mission-critical system using its GNAT Pro development environment. AAI Services Corporation utilized GNAT Pro as part of an overall upgrade to the U.S. Air Force T25 Simulator for Electronic Combat Training (SECT) system. The T25 SECT system is a software-based training aid that uses interactive combat laboratory exercises and simulated training missions to teach the principles of electronic countermeasures. As part of the upgrade, AAI Services updated one processor on the system’s student station from an SGI VME-based computer to a single board computer running Windows. The original software for the updated processor was ported to a different host and a new development station was added to the existing Training System Support Center.
BOSTON, Mass. – September 18, 2007 – Embedded Systems Conference – AdaCore, provider of the highest quality Ada tools and support services, today announced the immediate availability of GNATstack, a static analysis tool that helps developers predict the maximum stack usage requirements for their applications. GNATstack is available separately or as part of AdaCore’s GNAT Pro High-Integrity Edition products, supporting development for DO-178B, DO-278 and other related safety-critical standards.
BOSTON, Mass., September 18, 2007 - Embedded Systems Conference - AdaCore, provider of the highest-quality Ada tools and support services, today announced its second High-Integrity Edition product GNAT Pro High-Integrity Edition for Servers. The High-Integrity Family was first introduced in June of 2007 with the release of High-Integrity Edition for DO-178B, a product that supports safety-critical avionics and similar standards used in embedded software development. The new GNAT Pro High-Integrity Edition for Servers is fashioned to directly support DO-278, ESARR 4 and 6 and CAP670/SW01, the US, European and UK ground Air Traffic Management (ATM) safety-critical standards. Its capabilities can also be used to support any safety-critical, mission-critical or high reliability system requirements to run on a native platform.
PARIS and NEW YORK - September 10, 2007 - AdaCore, provider of the highest quality Ada tools and support services, today announced that its flagship GNAT Pro development environment is now available for Microsoft’s® .NET Framework. GNAT Pro's launch on .NET broadens AdaCore’s expanding portfolio of Microsoft platforms, which already includes releases for Windows 2000®, Windows 2003®, Windows XP®, and Windows Vista®. Now users of all major Microsoft platforms can also reap the productivity and reliability gains enabled by the Ada language from within the .NET Framework. This especially benefits those creating mission-critical applications, across a broad range of domains, including communications, financial software, and other enterprise systems.
NEW YORK and AMSTERDAM, Netherlands, March 7, 2007 - Avionics Exhibition and Convention - AdaCore, provider of the highest quality Ada tools and support, announces the first to market Ada 2005 language development environment, with the release of GNAT Pro version 6.0.1. Ada 2005, ISO/IEC 8652, was formally approved by ISO SC22/WG9 in January 2007. From the start AdaCore has actively participated in the ISO language standard revision process. This has enabled us to be at the forefront in supporting our customers and their use of the new Ada 2005 language standard.
PARIS, FRANCE - AdaCore, the leader in Ada solutions, today announced GNAT Pro Ada development tool suite support for Freescale Semiconductor, Inc.'s high-performance AltiVec® instruction set. The ability to access AltiVec instructions from Ada was initiated by MBDA, a world leading, global missile systems company. MBDA wanted to combine the potential power of AltiVec with the 'formality' of Ada. By adopting Ada, the programming language best suited for safety-critical, high-reliability applications, MBDA is supporting its own stated priority to "deliver the highest product reliability while developing innovative customized solutions."
NEW YORK, NY, USA - AdaCore announced today the availability of its GNAT Pro Ada development environment on Intel® Itanium® 2-based HP Integrity servers running either the HP-UX or Linux operating systems. With GNAT Pro, Ada users can take full advantage of the performance, security, and flexibility offered by the HP servers. And Ada users with applications running on the AlphaServer and PA-RISC platforms can look forward to a smooth transition to HP-UX 11i and Linux on HP's Integrity servers.
NEW YORK, NY, USA - Ada Core Technologies, the leader in Ada 95 solutions and providers of the GNAT Pro Ada development tool suite, today announced it is expanding its support agreement with Silicon Graphics (NYSE: SGI). The new agreement will include the development and support of the GNAT Pro product line on the SGI® Altix® family of superclusters and servers, which feature the 64-bit Intel® Itanium® 2 processor and the Linux® operating system.
Greg Gicca is presenting a paper “Meeting Top Safety and Security Requirements while Reducing Cost, Size, Weight, and Energy: Achieving High Assurance through a Verifiable Language on a MILS Architecture”.
This event is jointly organized with the IEEE Control, Aerospace and Electronic Systems Chapter and The University of Adelaide. Robert Dewar will give a talk discussing the topics below:
- Best practices for software design in critical systems. - The suitability of both existing and emerging standards. - An overview of tools and methodologies available to address the certification of such systems, including those available in the open source world. - Legal considerations and security. - A glimpse into the future.
Happy 20th Birthday, AdaCore!A Brief History of GNAT Pro 1 AdaCore and Safety CertificationA Brief History of SPARK ProInterview with Robert Dewar and Cyrille ComarA Brief History of CodePeerA Brief History of the GPS and GNATbench IDEsWorkshop on Medical Device Software SecurityUpcoming ReleasesPublic Ada Course, Spring 2015A Brief History of AdaCore and EducationNewsflashConferences/Events
Both SPARK and MISRA C are programming languages intended for high-assurance applications, i.e., systems where reliability is critical and safety and/or security requirements must be met. This document summarizes the two languages, compares them with respect to how they help satisfy high-assurance requirements, and compares the SPARK technology to several static analysis tools available for MISRA C with a focus on Frama-C.
This paper’s goal is to provide guidance on how to use Ada’s Object Oriented (OO) features for High-Integrity applications; i.e. high-reliability systems with requirements for safety and/or security which may need to demonstrate compliance with domain-specific certification standards.
Brief Overview
The paper was written by AdaCore experts with extensive experience in this area through their participation in industrial working groups such as EUROCAE’s WG-91, the DO-178C design committee, and ISO’s Ada Rapporteur Group that manages the Ada language standardization process. Another source of experience comes from the support of AdaCore customers, in domains such as aerospace and transportation, since the company’s inception in the mid 1990s. Many customers are using AdaCore tools during their certification process, and some have already completed the highest level of certification with Ada code while extensively using Object Oriented features.
The Object Orientation Concepts chapter summarizes the principal concepts in order to establish the terminology and provide criteria for comparing languages’ approaches. The Object Orientation in Ada chapter introduces Ada’s model for Object Orientation. Readers familiar with Ada 95 can move quickly to the last sections of this chapter, which describe several new features that are being added to the latest revision of language, known as Ada 2012, and which are extremely relevant to safe Object-Oriented programming. The next three chapters – Vulnerabilities and Their Mitigation, Complexity Management, and Safety and Verification Considerations – describe known concerns related to using Object Oriented technology in a High-Integrity environment and discuss recommended solutions. The final chapter, Directions for GNAT Pro Users, starts with a user checklist summarizing the steps we suggest taking when starting out in this area, and then presents the relevant elements and tools of the GNAT Pro technology.
The latest trend in our industry, “pervasive computing”, predicts the proliferation of numerous, often invisible, computing devices embedded in consumer appliances con- nected to the ubiquitous Internet. Secure, reliable applications combined with simplicity of use will make or break a company’s reputation in this market.
The Java “write once, run anywhere” paradigm, introduced by Sun in the mid- 90s, is embodied in a widely available computing platform targeting pervasive devices. Although the Java Virtual Machine was designed to support the semantics of the Java programming language, it can also be used as a target for other languages.
The Ada 95 programming language is a good match for the Java platform from the standpoint of its portability, security, reliability, and rich feature set. In this article we explain the features that have made Ada the language of choice for software-critical applications and how these features complement the Java programming language while increasing the overall reliability and flexibility of the Java platform.
AdaCore has developed strategic alliances and partnerships allowing customers to benefit from an ever-increasing complementary range of tools and services.
Trustworthy by Design -- Correct by Construction
Today, even vital infrastructures like power grids, classified government networks or company research sites tend to be connected to the Internet to take advantage of remote management and cloud services. Traditional approaches to securing these infrastructures rely on a strict isolation of critical systems from untrusted networks. In the presence of critical networked environments, other strategies are required to prevent unauthorized access which may be gained through the exploitation of errors in the complex software stacks that are used. One solution are component-based high-assurance platforms where untrusted software components are strictly isolated from security-critical functions on one single physical system.
IPsec relies on the correct operation of the Internet Key Exchange (IKE) protocol to meet its security goals. The implementation of IKE is a non-trivial task and results in a large and complex code base. This makes it hard to gain a high degree of confidence in the correct operation of the code.
The DSP group at the University of Udine is developing PPETP (Peer-to-Peer Epi-Transport Protocol), a new streaming protocol based on a peer-to-peer approach that will allow to distribute efficiently live multimedia material to a large number of users. Initially aimed to the specific application of multimedia streaming, the protocol evolved with time and now it can be considered a general-purpose overlay multicast protocol with many features (e.g., efficient use of bandwidth, NAT-traversal built-in procedures, countermeasures against security issues specific to peer-to-peer networks) that make it suitable for efficient multimedia streaming.
Dr. Martin C. Carlisle (former director of the Academy Center for Cyberspace Research at the USAF Academy, and now at Carnegie Mellon University) and Dr. Barry Fagin (US Air Force Academy) have developed a secure DNS server using Ada and the SPARK formal methods tool set. IRONSIDES is an authoritative DNS server that is provably invulnerable to many of the problems that plague other servers. It achieves this property through the use of formal methods in its design, in particular the language Ada and the SPARK formal methods tool set. Code validated in this way is provably exception-free, contains no data flow errors, and terminates only in the ways that its programmers explicitly say that it can. These are very desirable properties from a computer security perspective.
In the previous two Gems, we saw how aspects Static_Predicate and Dynamic_Predicate can be used to state properties of objects that should be respected at all times. This third and final Gem in the series is concerned with an aspect called Type_Invariant.
Let's get started…An overflow error occurs when the capacity of a device is exceeded. Overflow errors are a source of quality and security concerns. For instance, when an arithmetic overflow occurs, a calculated value does not fit in its specified size, and the calculation (and the program) just stops. Buffer overflow happens when a process stores data in a buffer outside of the memory that the programmer set aside for it. Buffer overflow errors are widely known to present a vulnerability to malicious hackers, who might exploit the error to sneak their own code onto a victim's disk, storing it outside of the intended buffer.
Let's get started…Input validation ensures that your program's input conforms to expectations - for example, to ensure that the input has the right type. But validation requirements can be much more complicated than that. Incorrect input validation can lead to security and safety problems since many applications live in a "hostile" environment and the input might be constructed by an attacker. "It's the number one killer of healthy software..." according to the CWE/SANS list of the top twenty-five most dangerous programming errors.
Let's get started…Note: This series of Gems makes references to SPARK and the Tokeneer project, which you can find out more about by visiting http://www.adacore.com/home/products/sparkpro/tokeneer/. See also the SPARK tutorial at http://www.adacore.com/home/products/sparkpro/tokeneer/discovery/.
Let's get started…
In the last Gem, we proved that procedure Linear_Search was free from uninitialized variable accesses and run-time errors, which are safety properties of Linear_Search.
Let's get started…
With Altran and AdaCore now teaming up to offer an integration of SPARK technology inside GPS (see http://www.adacore.com/home/products/sparkpro/), many GPS users will be interested in trying out the proof capabilities of SPARK on their own Ada programs. Of course it's a little more involved than that. SPARK is not only a set of tools for verifying high-assurance systems, but also incorporates a language that must be learned.
Let's get started…For some applications, especially those that are safety-critical or security-critical, it is essential that the program be correct, and that correctness be established rigorously through some formal procedure. For the most severe safety-critical applications the consequence of an error can be loss of life or damage to the environment. Similarly, for the most severe security-critical applications the consequence of an error may be equally catastrophic such as loss of national security, commercial reputation or just plain theft.
Let's get started…A program that doesn't communicate with the outside world in some way is useless although very safe. Such a program might almost be in solitary confinement. A prisoner in solitary confinement is safe in the sense that he cannot hurt other people but he is equally of no use to society either.
Let's get started…The aim of this booklet is to show how Ada 2005 addresses the needs of designers and implementers of safe and secure software. The discussion will also show that those aspects of Ada that make it ideal for safety-critical and security-critical application areas will also simplify the development of robust and reliable software in many other areas.
AdaCore’s tools and services are the ideal choice for developing large, long-lived Air Traffic Management systems, where safety and security is paramount.
NEW YORK and PARIS and BURLINGTON, Mass., November 15, 2017 – AdaCore Tech Days – AdaCore today announced that MDA, a business unit of Maxar Technologies, has selected the GNAT Pro Assurance Ada development environment for the LEON3 target processor, to produce the software for a Ku-Band communication subsystem that will replace the current version. This critical International Space Station (ISS) subsystem has to work reliably over the long term, a requirement that led MDA to maintain Ada as the implementation language. With GNAT Pro Assurance, a service known as sustained branches allows MDA to continue developing and maintaining their software over the long term using a specific version of the GNAT Pro technology, with access to code generator updates to correct critical issues.
AdaCore software development and verification tools help Real Heart deliver the high assurance, safety, and reliability that lifesaving medical devices demand.
AdaCore’s advanced software development and verification tools help enhance the safety and security of automotive, autonomous, and advanced driver-assistance systems while facilitating future technology upgrades and requirements.
The High Integrity Language Technology is focused on the cyber-resilience needs of critical software systems, where such a system must be trusted to maintain a continual delivery of services, as well as ensuring safety in its operations. Such needs have common goals and shared strategies, tools, and techniques, recognizing the multiple interactions between security and safety.
This workshop is designed as a forum for communities of researchers and practitioners from academic, industrial, and governmental settings, to come together, share experiences, and forge partnerships focused on integrating and deploying tool and language combinations to address the challenges of building cyber-resilient software-intensive systems. The workshop will be a combination of presentations and panel discussions, with one or more invited speakers.
AdaCore is an active actor and part of the Organizing and Program Committees.
The High Integrity Software Conference will take place in Bristol on 6November 2018. Now entering its fifth year, the conference continues to be the premier annual forum for the sharing of challenges, best practice and experience between software engineering practitioners – for software that matters. This mission continues to grow in importance, with 2018 having once again been a year in which software fallibility, cybersecurity breaches and the loss of public trust in autonomous systems have made headlines.
The need for safe and secure software — including Medical Device software — is becoming more important as cybersecurity threats in the healthcare sector become more frequent and severe. Beyond increasing the reliability, safety and security of their software, Ada and SPARK programming language adopters are also looking at controlling and reducing costs. Hillrom migrated to Ada and SPARK to verify the safety of the code by formally proving some properties, and improving its efficiency by removing dynamic checks, all the while keeping development and verification costs down. Read the full case study to find out more.
AdaCore’s technology provides the assurance that medical device developers, regulators, doctors and patients need so they can focus on saving human lives.
PARIS & NEW YORK & BRISTOL, UK, 14 August 2019 - AdaCore, a trusted provider of software development and verification tools, today announced the opening of AdaCore Ltd, which will serve as the company’s UK centre-of-excellence for the development of safety- and security-critical software tools.
AdaCore and Altran today announce their renewed sponsorship of the annual High Integrity Software (HIS) Conference, taking place in Bristol on November 5th, 2019. Now in its sixth year, the event attracts leaders in industry and academia who share the common focus of producing high integrity software. This promises to be the pivotal event as we enter an age of digital dependency, and many aspects of our everyday lives rely on the correct behaviour of software-intensive electronic systems. The event addresses new, current and future challenges and continues to grow year on year. It welcome an international audience, with delegates from continental Europe to Japan. Recognising the need to engage new engineers on this key topic, there are special rates available for those at an early stage of their career.
NEW YORK & PARIS & NEWPORT, Wales, September 24, 2019 - UK Space Conference - AdaCore, a trusted provider of software development and verification tools, today announced that the European Space Agency (ESA) has selected AdaCore to provide a qualified multitasking solution for spacecraft software development to support multiple ongoing and future ESA projects.
This paper presents initial, positive results from using SPARK to prove critical properties of OpenUxAS, a service-oriented software framework developed by AFRL for mission-level autonomy for teams of cooperating unmanned vehicles. Given the intended use of OpenUxAS, there are many safety and security implications; however, these considerations are unaddressed in the current implementation. AFRL is seeking to address these considerations through the use of formal methods, including through the application of SPARK, a programming language that includes a specification language and a toolset for proving that programs satisfy their specifications. Using SPARK, we reimplemented one of the core services in OpenUxAS and proved that a critical part of its functionality satisfies its specification. This successful application provides a foundation for further applications of formal methods to OpenUxAS.
NEW YORK & PARIS, February 18, 2020 - AdaCore today announced that three of its signature software development/verification tools for Ada, SPARK and C have been qualified under the ISO 26262 and IEC 61508 functional safety standards. AdaCore has over two decades of certification experience in safety-critical domains such as avionics, space, and rail. By completing the qualification process for automotive and industrial standards, the company has shown that its high integrity technologies can meet the demanding assurance requirements of the software-intensive automotive industry.
The size and complexity of software in embedded systems are growing at an astonishing rate. From aircraft and automobiles to medical devices, home appliances, and our homes themselves, products that were once hardware-only are now cyber-physical: they rely on software for much of their functionality. And we rely on that software for the dependability of those systems, especially their safety and security. This increasing complexity is driving technology leaders to adopt formal methods.
This course introduces you to the Ada language by comparing it to C. It assumes that you have good knowledge of the C language. It also assumes that the choice of learning Ada is guided by considerations linked to reliability, safety or security. In that sense, it teaches you Ada paradigms that should be applied in replacement of those usually applied in C.
This course also introduces you to the SPARK subset of the Ada programming language, which removes a few features of the language with undefined behavior, so that the code is fit for sound static analysis techniques.
This course was written by Quentin Ochem, Robert Tice, Gustavo A. Hoffmann, and Patrick Rogers and reviewed by Patrick Rogers, Filip Gajowniczek, and Tucker Taft.
AdaCore is a Principal Member of The Open Group’s Future Airborne Capability EnvironmentTM (FACE) Consortium. We have been actively involved with the FACE effort since 2012, participating in and contributing to both the Technical and Business Working Groups.
Our objective in the FACE Consortium is to help FACE software suppliers meet assurance requirements for reliability, safety, and security while realizing the portability and reusability benefits that come from FACE conformance. Among the languages that are called out in the FACE Technical Standard – C, C++, Ada and Java – the one that best promotes high assurance coupled with code portability is Ada.
As a software tool provider to the Aerospace and Defense community, we offer products that enable and encourage FACE software suppliers to use Ada for their applications. More specifically, AdaCore’s FACE related products include:
GNAT Pro Ada development environments targeted to RTOSes supplied by FACE Consortium members, such as Wind River’s VxWorks 653 and Lynx Software Technologies’ LynxOS-178;
Efficient run-time libraries that are distributed with our cross-compilation environments and have been deployed in avionics systems certified at the highest Design Assurance Levels (DALs) of software standards such as DO-178B/C; and
Static analysis tools including the formal methods-based and CWE-compatible SPARK Pro toolsuite, the CWE-compatible CodePeer deep static analyzer for Ada, and the GNATcheck coding standard verifier for Ada.
This book summarizes AdaCore’s technologies and shows how they can help avionics suppliers develop and verify high-assurance FACE conformant software. The discussion is based on Edition 3.1 of the FACE Technical Standard and applies also to earlier versions.
Ada and its subset SPARK, a language inspired by Pascal, embedding capabilities to describe specification, implementation and verification in one platform
SPARK is a software development technology (programming language and verification toolset) specifically designed for engineering ultra-low-defect-level applications, for example where safety and/or security are key requirements. SPARK Pro is the commercial-grade offering of the SPARK technology developed by AdaCore, Altran and Inria.
SPARK has an extensive industrial track record. Since its inception in the late 1980s it has been used worldwide in a range of industrial applications such as civil and military avionics, air traffic management/control, railway signaling, cryptographic software, cross-domain solutions, medical devices and automotive.
The SPARK language is a large subset of Ada 2012. SPARK includes as much of Ada as is possible/practical to analyze formally, while eliminating sources of undefined and implementation- dependent behavior. SPARK includes Ada’s program-structure support (packages, generics, child libraries), most data types, safe pointers, contract-based programming (subprogram pre- and postconditions, scalar ranges, type/subtype predicates), Object-Oriented Programming, and the Ravenscar subset of tasking features.
CYBERUK is the UK Government’s flagship cyber security event which AdaCore will be attending to demonstrate expertise in military-grade cyber-secure system design at exhibition booth A68.
AdaCore, a trusted provider of software development and verification tools, today announced the launch of its new RecordFlux technology, designed to ease the development and security of binary communication protocols. The technology comprises a Domain Specific Language (DSL) to precisely describe complex binary data formats and communication protocols, and a toolset to verify specifications and generate provable SPARK code that can be executed on a target CPU.
One of the basic requirements for enterprise platform security is device attestation: trustworthy evidence of a device’s identity and security properties. The industry standard Security Protocol and Data Model (SPDM) addresses this need, defining message formats and session behaviors that device suppliers can implement for attestation.
This paper explains how AdaCore partnered with NVIDIA to capture and implement a subset of the SPDM 1.1.0 specification, using AdaCore’s RecordFlux product in conjunction with the SPARK/Ada programming language and the SPARK Pro toolsuite. The project successfully demonstrated that these technologies can address the vulnerabilities that communication protocols and complex data formats can bring, and the SPDM library that the project produced will be integrated into the firmware of microcontrollers and microprocessors that NVIDIA designs
AdaCore, a trusted provider of software development and verification tools, today announced it has committed books, resources, and training in support of BAE Systems’ engineering apprenticeship programme, demonstrating its role as a dedicated partner and its commitment to the advancement of high integrity software.
The Ada Europe conference schedule comprises a journal track, an industrial track, a work-in-progress track, a vendor exhibition, parallel tutorials, and satellite workshops.
AdaCore is sponsoring this event and will be giving two talks:
Patrick Rogers will present "An Update On the Tasking Profiles in Ada 2022"
Paul Butcher will present " ‘Security Hardening Ada Programs through Innovative Fuzz Testing"
Electronic election systems need to be demonstrably secure in order to ensure the protection of votes, the privacy of voters, and the prevention of interference. That’s why Software Improvements selected the Ada 2012 programming language and AdaCore’s GNAT Pro Ada development environment to upgrade the Australia Capital Territory’s Electronic Voting & Counting System (eVACS®), a public-facing system that demands a high level of security.
Discover Enhanced Software Security with SPARK Pro! Dive into our exclusive webinar featuring Yannick Moy, and learn about the cutting-edge features of SPARK Pro with live demonstrations on pointer ownership, function contracts, and secure type casting.
Battery Ventures, a global, technology-focused investment firm, today announced a significant investment in AdaCore, a leader in providing software development tools for safety- and security-critical systems. This strategic partnership will catalyze AdaCore's expansion, positioning the company as the go-to source for high-integrity, software-development tooling.
AdaCore, a leader in high-assurance, safe, and secure software toolchains, is set to stand out at CYBERUK by showcasing its unique approach to Secure Avionics by Design (SAbD).
AdaCore is thrilled to be part of the Safety-Critical Rust Consortium alongside The Rust Foundation, Arm, Ferrous Systems, OxidOS, HighTec EDV-Systeme GmbH, TrustInSoft, Veecle, and Woven by Toyota. The primary objective of this group will be to support the responsible use of the Rust programming language in safety-critical software — systems whose failure can impact human life or cause severe environmental or property harm.
For 30 years, AdaCore has provided the essential tools for building reliable, safe, and secure software. Throughout these decades, the Ada programming language and freely licensed open-source software have been integral to AdaCore's mission.
AdaCore is excited to announce its participation in the SCHEME research project. Rolls-Royce has assembled a world-class consortium of UK industry and academia to deliver the next generation of high-integrity processing platforms for use in aerospace and other harsh environments.
Rapita Systems will demonstrate the integration of their RapiCover Zero and RapiTime Zero tools with AdaCore’s GNAT Pro for Rust next week at the High Integrity Software Conference (HISC). The integration will show how structural coverage and execution time metrics, including worst-case execution time, can be collected during on-target tests of safety-critical code written in Rust.
Explore the advantages of Ada, SPARK, and Rust over C/C++ for high-integrity software. This paper highlights the safety, security, and efficiency of each language, covering ecosystems, community support, and adoption costs. Discover the best fit for your projects to reduce errors and boost software integrity. Download now for strategic insights.
Do you need to meet ISO 26262 qualification requirements? AdaCore’s development tools provide solutions for guaranteeing the safety of automotive software.
Explore how Ada, SPARK, and Rust address critical memory safety challenges in our latest whitepaper. Memory safety issues account for over 70% of security vulnerabilities in major tech systems, making robust solutions essential. This paper discusses common bugs like out-of-bounds writes and null pointer dereferences, and demonstrates how the unique features of these programming languages significantly reduce risks and enhance system reliability. Discover how adopting these memory-safe languages can fortify your software against pervasive security threats, enabling you to develop complex systems with greater confidence and security. Download now to learn more.
The Rust Foundation is an independent non-profit organization dedicated to stewarding the Rust programming language, nurturing the Rust ecosystem, and supporting the set of maintainers governing and developing the project.
AdaCore, a leader in high-integrity software development tools, is excited to announce its participation in Embedded World 2025, which will take place from March 11th to 13th in Nuremberg, Germany. This year, AdaCore will showcase its cutting-edge solutions for safety and security-critical embedded systems, with a special focus on SPARK and Rust technologies.
AdaCore is well-known for its support of high-integrity embedded development. When a new language, Rust, emerged and started making claims about memory safety and minimal footprint, it was only a matter of time before it found its way into the AdaCore family.
Discover how to Prove Security and Safety for Embedded and Systems Software. Learn about what SPARK is, how SPARK works, and see how SPARK can be applied to a M.A.R.S. Rover to prove safety during this webinar hosted by AdaCore’s Head of Product and Innovation, Tony Aiello.
Software recalls in the automotive industry are rising, with safety now a critical business concern. This paper explores how Ada and SPARK, through formal verification, enable compliance with ISO 26262, reduce defects, and strengthen both safety and security. Learn how NVIDIA leveraged SPARK to achieve the highest levels of assurance—and why it can help your organisation do the same.
DevSecOps offers the promise of delivering solutions faster, with higher quality, and more security. The challenge is how to build safe code, at scale, while going fast. Join AdaCore Product Manager, Sean Evoy, to learn how to integrate CodeSonar and static application security testing in your DevSecOps pipeline and help your developers separate the needles from the hay.
Webinar Time: 16:00 GMT | 17:00 CET | 11:00 EST | 8:00 PST
Lauterbach's TRACE32® is the industry's first development tool suite to fully support the AdaCore GNAT Pro Ada compiler, which is designed for safety-critical applications in the fields of avionics, automotive, and defense. This enables debugging of compiled Ada programs at the source code level, even in multithreaded applications, and Code Coverage measurements for certifications.
