A recently published paper by the National Institute of Standards and Technology (NIST), examines software assurance tools as a fundamental resource to improve quality in today’s software applications. It looks at the behavior of one class of software assurance tool: the source code security analyzer. Because many software security weaknesses are introduced at the implementation phase, using a source code security analyzer should help reduce the number of security vulnerabilities in software.
We have posted a new paper to the Open-DO website “High-Integrity Object-Oriented Programming in Ada“. 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. The paper’s authors have extensive experience in this area through their participation in industrial working groups such asthe joint EUROCAE WG71 / RTCA SC 205 working group defining the upcoming RTCA DO178-C/EUROCAE ED12-C avionics safety standard, and ISO’s Ada Rapporteur Group that manages the Ada language standardization process. More information can be found at http://www.open-do.org/high-integrity-oo-programming-in-ada/
We expect this document to evolve over time, so we kindly ask readers to provide as much feedback as possible to AdaCore at info@open-do.org with the name of the document mentioned on the subject line.
The Real Time Linux Workshop 2011 will be held in Prague, October 20 to 22. The call for papers is now out with several topics of interest including “Safety-related FLOSS systems”. More details on the CFP and event can be found on the website:
We learned this week of ImProve, a lightweight DSL intended for building high assurance embedded applications. Developed by Tom Hawkins, the tool is an EDSL that performs formal verification (via. model checking) and code generation. The host language is Haskell; meaning ImProve programs are nothing more than Haskell programs that call the ImProve library API.
ImProve’s semantics are extremely simple:
- It is an imperative language like C or Ada.
- It only has 3 datatypes (bool, int, float).
- There are a total of 16 expression types (add, subtract, AND, OR, etc.).
- Statements consist of variables assignments, conditional “IF” statements, and assertions.
In terms of the ImProve compiler structure, a thin layer of Haskell helps translate ImProve programs down to an intermediate representation, from which programs are verified and C code is generated.
For verification, the IR language is passed to a k-induction model checker (part of the ImProve library), which makes calls down to an SMT solver (currently Yices). ImProve provides assertions statements to capture design intent. Assertions can be seeded with previously proven lemmas to aid verification convergence.
For more information, please visit the project website:
A number of very interesting articles in February’s SoftwareTech News look at the use of FLOSS by the DoD. Topics below give an insight the DoD’s position and strategy in employing open source software.
Software is a Renewable Military Resource
Military Open Source Community Growing
Evaluating Open Source Software
Open Source Software Is Commercial
Implementing Open Standards in Open Source
Running Open Technology Development Projects
Publicly Releasing Open Source Software Developed for the U.S. Government
Ever found yourself in an extreme stressed state because of some bugs* escaping you? Then you know how it feels to be Elmer Fudd. Not a typical hero, never victorious in his hunt. So it feels being a software engineer. A new episode in this tragicomedy is a paper by Yang et al. from Uni Utah that will be presented at PLDI conference this year.
In this paper, the authors report on 3 years looking for bugs in C compilers. They generated random compliant ANSI C programs, which all C compilers should compile to a program computing the same values, and compared the results of various C compilers on the generated programs. They found 325 bugs, 8 of which they present in a few lines in the paper. Really savory to see how logic defeats man. In case you chill like me over these bug stories, you can read some I wrote at Microsoft and at AdaCore.
The light in the dark comes from a little known C compiler, CompCert whose middle-end successfully defeated the repeated attacks (6 CPU-years!) of the researchers. Guess what? It is written in Coq, a formal language, which allowed proving its correctness. Also interesting is the fact that even CompCert had bugs in its non formally verified parts, like the parser, where it makes sense to have testing in place.
From a talk given at the SPARK User Group 2010 High Assurance Software Symposium, Rod Chapman from Altan Praxis talks about the guiding principles behind PSP (Personal Software Process) and TSP (Team Software Process).
Below are the slides from the recent Couverture project conclusion meeting. Cyrille Comar presented the original needs and goals of the project, the challenges the team came across a long the way, and the main results.
At the upcoming Embedded World conference in Nuremberg, Germany, there will be a days conference on the use of freely-licensed open source software (FLOSS) to build safety-critical systems. Presentation topics include:
Validation of Linux for Safety-Related Systems
Linux as a real-time Hypervisor for the automotive industry
Efficient Safety Critical Systems Development – Is FLOSS the only answer?
Finding Misuses of Unsigned Integers in Linux Device Driver Code
“Open Proof” for Railway Safety Software A Potential Way-Out of Vendor Lock-in Advancing to Standardization, Transparency, and Software Security
Improved Redundancy and Consistency beyond RAID 1
Utilizing security methods of FLOSS GPOS for safety