• Video
  • 22-May-2012 02:16 EDT

Building Security In: The SPARK Approach to Software Development


Purchase Required to View Video

Short Preview Below

Software products in the automotive industry are by nature widely distributed and costly to update (recall), so high reliability is clearly of utmost importance. Just as clearly, the increasing reliance on remote access to such systems, for diagnostic and other purposes, has made security an essential requirement, and traditional techniques for software development are proving to be inadequate in dealing with these issues. Correctness by Construction is a software design and development methodology that builds reliability and security into the system from the start. It can be used to demonstrate, with mathematical rigor, a program's correctness properties while reducing the time spent during testing and debugging. This paper will discuss the use of Correctness by Construction, and its accompanying SPARK language technology, to improve automotive systems' security and reliability. (The approach can also account for safely issues, although that is not the focus of this paper.) The SPARK language and toolset avoid vulnerabilities found in other languages and can, for instance, guarantee the absence of run-time errors such as divide-by-zero or buffer overflow. Using the SPARK language and toolset, developers can verify secure information flow through the system and, more generally, demonstrate that security-related properties are achieved. The approach offered by Correctness by Construction and SPARK is in contrast with the use of so-called retrospective static analysis tools that attempt to find errors or vulnerabilities in existing code. Such tools can only demonstrate the presence of errors (which may be correctable) but cannot show how many errors remain in the system. With Correctness by Construction and SPARK, developers can ensure that errors and vulnerabilities are not introduced in the first place. Correctness by Construction and SPARK have a growing success rate in applications where failure is not tolerated and where demanding safely or security standards must be met. The technology has been adopted in safety-critical domains including avionics, air traffic control, and rail transportation, and likewise in systems that must meet the highest security levels defined in the Common Criteria (Evaluation Assurance Levels (EAL) 4 through 7). This paper discusses how to apply Correctness by Construction and the SPARK technology to improve the reliability and security of automotive systems while reducing the costs of development, debugging, and maintenance. It includes examples of previous high-security systems that have been developed using this approach and discusses the applicability of the techniques to automotive systems.

Stuart Matthews

Purchase to View
Learn More
Technical Paper / Journal Article
HTML for Linking to Page
Page URL
Rate It
No ratings yet

View More Video

A new index for evaluating load path dispersion is proposed, using a structural load path analysis method based on the concept of U* , which expresses the connection strength between a load point and an arbitrary point within the structure enables the evaluation of the load path dispersion within the structure by statistical means such as histograms and standard deviations. Presenter Tadashi Naito, Honda R&D Co., Ltd.
By introducing the concept of a separation between graphics and logic, interpreted run time architecture, and defined communication protocol, the ARINC 661 standard has addressed many of the concerns that aircraft manufacturers face when creating cockpit avionics displays. However, before kicking off a project based on the standard, it is important to understand all aspects of the standard, as well as the benefits and occasional drawbacks of developing with ARINC 661 in mind. This white paper will first provide an overview of ARINC 661 to clarify its concepts and how these relate to the development process. The paper will also describe the benefits of using a distributed development approach, and will outline practical, real world considerations for implementing an ARINC 661-based solution. Finally, readers will learn how commercial tools can be used to simplify the creation of displays following the standard to speed development and reduce costs.
In any new aircraft development program there are many important design decisions that determine profitability potential. The key to making new aircraft profitable is to design features that will command more money than the cost to provide them within the market's ability to absorb them. The business model in this paper shows how to predict or find: 1) the costs to provide various aircraft features; 2) the values that aircraft buyers place on these features; 3) the amount of money that buyers have to commit to them, 4) the open spaces in the market in which to place new designs and 5) the predicted profits from new designs. In this process, this paper extends previous work on the law of value and demand, which states that attributes determine value; value determines price; and that price determines demand. This four-dimensional, non-negative system hosts a business model that describes the features needed to enable aircraft designs to go from concepts to profitable assembly lines.
As a result of recommendation from the Augustine Panel, the direction for Human Space Flight has been altered from the original plan referred to as Constellation. NASA's Human Exploration Framework Team (HEFT) proposes the use of a Shuttle Derived Heavy Lift Launch Vehicle (SDLV) and an Orion derived spacecraft (salvaged from Constellation) to support a new flexible direction for space exploration. The SDLV must be developed within an environment of a constrained budget and a preferred fast development schedule. Thus, it has been proposed to utilize existing assets from the Shuttle Program to speed development at a lower cost. These existing assets should not only include structures such as external tanks or solid rockets, but also the Flight Software which has traditionally been a ?long pole? in new development efforts. The avionics and software for the Space Shuttle was primarily developed in the 70's and considered state of the art for that time.

Related Items

Training / Education