Using model-driven development to reduce system software security vulnerabilities
Editor’s Note: This article is based on material contributed by Guy Broadfoot to Embedded Systems Security, by David and and Mike Kleidermacher. He outlines how many features of model-driven development tools can also be used to create reliable software code for security- and safety-critical applications.
The majority of embedded software developers using traditional programming languages such as C and C++ make use of processes and techniques inherent in the language to improve reliability and reduce security flaws. However, another approach that has met with increasing success is the use of model-driven design (MDD).
The premise of MDD is to raise the abstraction of software development from the low-level imperative programming language that is fraught with opportunities to shoot one’s self in the foot to a higher-level modeling language that reduces the distance between design and implementation and by doing so reduces the flaws that lead to security and safety failures.
Modeling lends itself better to formal proofs of specifications and security policies than do traditional programming languages. Indeed, a side benefit of using some MDD platforms – especially the ones that support formal methods and automatic code generation - is the ability to make formal arguments regarding the correspondence between specification, design, and implementation, a core challenge in all formal approaches. The following will deal with MDD methods that lend themselves to formal analysis and therefore raise the assurance of quality, safety, and security.
In discussions about MDD and MDD platforms, the term verification tends to mean different things to different people. According to the IEEE, the term verification is given the following two definitions:
- The process of evaluating a system or component to determine whether the products of a given development phase satisfy the conditions imposed at the start of that phase.
- Formal proof of program correctness.
Most MDD vendors assume the first definition for the term, so throughout this article, we do the same. And in cases in which formal proof of program correctness is intended, we use the term formal verification.
This distinction is important: many MDD platforms offer facilities for verification, usually in the form of simulating execution on the development host before testing it on the target system. Test case generation features often support this activity. However, few MDD platforms offer facilities for formal verification to provide proof of correctness of a software design, and for those that do, this is an important distinguishing capability. Where these facilities exist, they offer great benefits, especially in multi-threaded and multicore designs.
We use the term ‘component’ to mean some physical hardware or software element of a system that satisfies one or more interfaces. We regard a system as comprising a collection of components. The term subsystem is a modeling concept defining the grouping of related components and/or other subsystems. It is a modeling abstraction to assist in the stepwise partitioning of large and complex systems. The physical realization of a subsystem is always by means of the components that it comprises.
Software development methodologies historically have tended to concentrate on tools that assist the software developer with system composition, integration, and especially testing. Various component-based technologies, such as CORBA and Microsoft’s COM, DCOM, and .NET have aimed at increasing software development productivity and quality by improving reuse through component abstraction in those domains where the technologies are applicable. Although increasingly sophisticated development tools such as optimizing compilers, source language debuggers, test generators, and test execution platforms have long been available to help software developers with implementation and testing, this conventional way of developing software is increasingly challenged by:
- the relentless pressure to reduce time to market and introduce new products in ever-shorter cycles, frequently leading to hardware and software being developed in parallel and final hardware platforms not available during most of the time the software is under development;
- the increasing complexity of embedded software, as essential product characteristics and end-user value are realized by software;
- the introduction of multi-core technologies, creating an environment in which software design and coding errors are more likely and conventional testing techniques are less effective;
- the continuing downward pressures on development costs;
- the trend toward distributed development sites, often in different time zones.
All these challenges must be met while achieving ever-higher quality levels to meet rising user expectations and regulatory pressures.
Conventional software development is labor intensive and bounded by human error. According to a recent Venture Development Corporation survey, software labor costs account for more than 50% of the total spent on embedded system development. Of this spending, according to Ebert and Jones, typical industry experience finds up to 40% spent on testing and rework. It is hard to think of another engineering domain that habitually spends 40% of its development budget identifying and removing defects that shouldn’t have been present in the first place.
Historically, organizations have attempted to address some of these issues by means of process improvement - that is, by introducing practices, procedures, and standards governing every aspect of specification, design, implementation, and testing. While some of this rigor is required in any high-assurance and high security development process, MDD can help to reduce that overhead, enabling higher assurance while improving developer efficiency.
Decreased efficiency due to development process overhead leads rapidly to diminishing return on investment and unsurprisingly to a loss of interest by senior management. Finally, beyond a relatively small threshold of complexity and size of a component, it is simply not feasible to try to achieve high-assurance security and safety with traditional software development techniques. MDD is a tool to address this scalability problem, enabling software developers to be more productive and deliver products more quickly and with significantly fewer defects.
What Is MDD?
MDD is based on the systematic use of models as primary artifacts throughout the software engineering life cycle. MDD aims to elevate functional models to a central role in the specification, design, integration, and validation of software.
In conventional software development, the definitive statement of software function is a mixture of informal functional requirements documents and the program source code. Establishing the correspondence between the two is often difficult. By raising the abstraction level in which specifications and designs are expressed, MDD aims to replace the specification and source code approach with a functional model expressed in an unambiguous, precise modeling language that can be understood by both the domain experts who determine what the resulting system does and the software developers who implement it. Additionally, code generated automatically from the model assures correspondence between specification and implementation.
MDD uses models to represent a system’s elements, the structural relationships between them, and their behavior and dynamic interactions. Modeling structural relationships supports design exploration and system partitioning; modeling behavior and interactions is essential for being able to verify designs by verifying models and for code generation. In practice, these last two points are the source of most of the benefits claimed for MDD.
But for many embedded software developers, code generation in particular seems to be difficult to accept. However, without code generation, much of the advantage of MDD is lost; in reality, deciding to adopt an MDD approach means accepting automatic code generation from models.
Models must be expressed in a modeling language with a formally defined grammar and semantics capable of expressing both static structure and dynamic behavior at an abstract level removed from the programming domain. We can divide these languages into two groups:
Vendor-specific language Languages developed and promoted by a specific vendor of an MDD platform such as MatLab and Simulink from MathWorks, Esterel from Esterel Technologies, and the ASD language (Figure 1 below) used in Verum Software Technologies’ ASD:Suite.
Standardized languages Languages that have been defined by industry groupings of interested users and MDD platform vendors. These are most commonly based on the Unified Modeling Language (UML).
Figure 1: Rather than coding, testing, and refining each component in separate steps, ASD Suite allows the developer to create an initial set of requirements. Based on this, the modeling tool captures both the external and internal behavior of the component using its two basic model types: interface models and design models. (Source: Vernum Software Technologies)
In practice, a significant difference between the vendor-specific modeling languages and the vendor-independent, UML-based languages is, of course, the degree of vendor lock-in that results from using them. The UML-based languages have the laudable goal of being vendor independent and, in principle, offering the possibility for models to be exchanged between platforms. Vendor-specific languages generally do not facilitate model exchange between platforms.
UML-based modeling languages are increasingly being adopted by MDD platforms (Figure 2) and other tools from several major vendors and are standardized.
Figure 2: The latest version of UML allows the developer to create 14 types of diagrams divided into two categories. For structural information it has seven diagram types, The second category is for general types of behavior and (Source: Wikipedia)
The quality of generated code and its suitability for a particular domain and use is an important consideration in choosing an MDD platform or even deciding to take the MDD route at all. We distinguish between two types of models, namely those that are executable and those that are both executable and formally verifiable.
The potential benefits of MDD
By raising the abstraction level in which specifications and designs are expressed and eliminating informal functional specifications, MDD has the potential to
- Eliminate specification and design errors early in the development cycle where they are cheapest and easiest to rectify
- Increase the degree of automation that can be applied to the development process by means of automatic code generation
- Facilitate parallel hardware/software design by enabling models to be verified by simulating execution behavior on development hosts before the target system is available
- Reduce the required testing effort by applying automated formal verification techniques to the functional models in combination with simulating execution behavior instead of relying solely on testing the implemented program code