Static Analysis in Flight-Critical Software
Scalable and Flexible Static Analysis of
Flight-Critical Software
Guillaume P. Brat Arnaud J. Venet
guillaume.p.brat@nasa.gov arnaud.j.venet@nasa.gov
Carnegie Mellon University
NASA Ames Research Center
Roadmap
•
Static analysis for flight-critical systems
•
Challenges of sound static analysis
•
IKOS: an open architecture for sound static
analyzers
•
Applications of IKOS
Roadmap
•
Static analysis for flight-critical systems
•
Challenges of sound static analysis
•
IKOS: an open architecture for sound static
analyzers
•
Applications of IKOS
Static Analysis
Code
Static
Analyzer
Defects
Certificates
of
Correctnes
s
Properties,
Invariants
Flight-Critical Code
•
Testing is insufficient
–
Impossible to explore all execution paths (A330 cockpit
display shutdown after 96 hours of operation due to an
arithmetic overflow)
–
Some errors may be hard to detect (memory
corruption due to a buffer overflow)
•
Static analysis brings a new level of assurance
–
Soundness
is important
Soundness
•
Unsound tools (Coverity, KlocWork, GrammaTech)
–
False negatives, false positives
–
Little parameterization required
•
Sound tools (MathWorks PolySpace, ASTREE)
–
No false negatives: formal verification
–
False positives
–
Parameterization is key to low false positive rate:
•
Bounds on inputs of the system
•
Specialization of the analysis algorithms
Roadmap
•
Static analysis for flight-critical systems
•
Challenges of sound static analysis
•
IKOS: an open architecture for sound static
analyzers
•
Applications of IKOS
The Specialization Conundrum
•
MathWorks PolySpace Verifier:
–
General purpose tool for embedded C/C++ code
–
Applicable to codes under 100 KLOC in practice
–
Manual review of warnings may be effort-intensive
•
ASTREE:
–
Scalable, yields zero or few warnings
–
Specialized for a restricted subset of C (single-
threaded, no dynamic memory allocation, no complex
pointer structure)
Building a Custom Static Analyzer
•
C Global Surveyor (developed in the RSE group at
NASA Ames Research Center)
–
Specialized for complex C code developed in the Mars
Exploration Program (Mars Pathfinder, MER)
–
Analyzes the whole MER flight system (550+ KLOC)
•
One-time exercise
–
Complete rewrite may be necessary when changing the
target code and/or properties analyzed
–
Significant expertise required
What do we need?
•
A static analysis tool with an open architecture
–
Access to the algorithms
–
Possibility of refining/specializing the way the tool
operates
•
A flexible API
–
We don’t want to rewrite the core analysis algorithms
–
But we want to be able to combine them in new ways
for a particular application
Roadmap
•
Static analysis for flight-critical systems
•
Challenges of sound static analysis
•
IKOS: an open architecture for sound static
analyzers
•
Applications of IKOS
IKOS: Flexible Static Analysis Design
•
I
nference
K
ernel for
O
pen
S
tatic Analyzers
–
A development platform for building static analyzers
–
Library of C++ classes encapsulating high performance
static analysis algorithms
–
A static analyzer is assembled from the building blocks
provided by IKOS
•
An effective buffer overflow analyzer for C
programs can be written in a few hundred lines of
C++ using IKOS
Flexible C/C++ Front-End
•
The untold story of using static analysis tools
–
Getting the code to just
parse
is a daunting task
–
The front-end of most static analysis tools expects
standard C/C++ code as an input, which is rarely the
case for embedded software
–
Significant changes to the build/code may be required
•
IKOS is based on the LLVM platform
–
The GCC compiler can compile just about any existing
code with little or no change
–
GCC can generate LLVM assembly code
Static Analysis Design with IKOS
GCC
C/C++
Code
LLVM
Analyzer
Verifier
Properties
Verification
Report
Interval
Domain
Pointer
Analysis
Decision Procedure
Fixpoint
Iterator
Octagon
Domain
…
…
IKOS
Example
•
The analysis discovers program properties:
–
0 ≤
i
≤ 7
–
p
points to fourth element of structure
S
void f(
double *p, int n
) {int i;
for (i = 0;
i < n
; i++) {p[i] = ...;
}
}
...
f(
&S[3], 8
);
...
Example
•
The verification uses the properties discovered:
–
Array-bound compliance
–
Check that structure
S
has at least 11 elements
void f(
double *p, int n
) {int i;
for (i = 0;
i < n
; i++) {p[i] = ...;
}
}
...
f(
&S[3], 8
);
...
Access within bounds?
Specialization of the Analyzer
•
Specialization consists of finding the right blend
of algorithms
–
To compute strong enough properties for the verifier
–
And
guarantee reasonable analysis times
•
This is an intrinsically empirical process
–
IKOS allows the analysis designer to easily swap
abstractions and decision procedures
–
IKOS helps streamline the design of specialized static
analyzers
Roadmap
•
Static analysis for flight-critical systems
•
Challenges of sound static analysis
•
IKOS: an open architecture for sound static
analyzers
•
Applications of IKOS
Verification of UAS Autopilots
•
Certifying the flight software of unmanned
aircrafts is critical for NextGen
–
Complex code bases
–
Variety of platforms and architectures
–
No standard development process like DO178
•
Static analysis can help
–
Formal verification provides high assurance
–
Cost-effective, works on the code “as is”
Experiments with IKOS
•
Verification of array-bound compliance (NASA APG
milestone)
•
Benchmark of realistic UAS autopilots
•
Juliet is a cyber-security benchmark from NIST and
is listed here just to demonstrate the scalability of
the analyzer
MATLAB/Simulink Autocode
•
Auto-generated code from MATLAB/Simulink
models is increasingly used in critical flight
software
•
Static analysis can provide formal guarantees that
the autocode satisfies critical safety properties
•
We are currently developing a specialized analyzer
for this class of code using IKOS
Technical Infusion
•
Ongoing activities to transfer the technology into
NASA missions
Conclusion
•
Static analysis is an important tool for the
assurance of flight-critical software
•
There is no silver bullet: static analyzers need to be
specialized to be effective
•
IKOS is a step toward streamlining the design of
specialized high-performance static analyzers
Explore the challenges and advancements in static analysis for flight-critical systems, focusing on the importance of soundness and assurance through tools like IKOS, MathWorks PolySpace, and ASTREE. Learn about the limitations of testing in detecting critical errors and how static analysis can offer a new level of assurance. Discover the role of parameterization in reducing false positives and the specialization conundrum faced by tools like MathWorks PolySpace Verifier and ASTREE.
Download Presentation
Please find below an Image/Link to download the presentation.
The content on the website is provided AS IS for your information and personal use only. It may not be sold, licensed, or shared on other websites without obtaining consent from the author.If you encounter any issues during the download, it is possible that the publisher has removed the file from their server.
You are allowed to download the files provided on this website for personal or commercial use, subject to the condition that they are used lawfully. All files are the property of their respective owners.
The content on the website is provided AS IS for your information and personal use only. It may not be sold, licensed, or shared on other websites without obtaining consent from the author.
E N D
Presentation Transcript
Scalable and Flexible Static Analysis of Flight-Critical Software Guillaume P. Brat Arnaud J. Venet guillaume.p.brat@nasa.gov arnaud.j.venet@nasa.gov Carnegie Mellon University NASA Ames Research Center
Roadmap Static analysis for flight-critical systems Challenges of sound static analysis IKOS: an open architecture for sound static analyzers Applications of IKOS
Roadmap Static analysis for flight-critical systems Challenges of sound static analysis IKOS: an open architecture for sound static analyzers Applications of IKOS
Static Analysis Static Analyzer Code Certificates of Correctnes s Properties, Invariants Defects
Flight-Critical Code Testing is insufficient Impossible to explore all execution paths (A330 cockpit display shutdown after 96 hours of operation due to an arithmetic overflow) Some errors may be hard to detect (memory corruption due to a buffer overflow) Static analysis brings a new level of assurance Soundness is important
Soundness Unsound tools (Coverity, KlocWork, GrammaTech) False negatives, false positives Little parameterization required Sound tools (MathWorks PolySpace, ASTREE) No false negatives: formal verification False positives Parameterization is key to low false positive rate: Bounds on inputs of the system Specialization of the analysis algorithms
Roadmap Static analysis for flight-critical systems Challenges of sound static analysis IKOS: an open architecture for sound static analyzers Applications of IKOS
The Specialization Conundrum MathWorks PolySpace Verifier: General purpose tool for embedded C/C++ code Applicable to codes under 100 KLOC in practice Manual review of warnings may be effort-intensive ASTREE: Scalable, yields zero or few warnings Specialized for a restricted subset of C (single- threaded, no dynamic memory allocation, no complex pointer structure)
Building a Custom Static Analyzer C Global Surveyor (developed in the RSE group at NASA Ames Research Center) Specialized for complex C code developed in the Mars Exploration Program (Mars Pathfinder, MER) Analyzes the whole MER flight system (550+ KLOC) One-time exercise Complete rewrite may be necessary when changing the target code and/or properties analyzed Significant expertise required
What do we need? A static analysis tool with an open architecture Access to the algorithms Possibility of refining/specializing the way the tool operates A flexible API We don t want to rewrite the core analysis algorithms But we want to be able to combine them in new ways for a particular application
Roadmap Static analysis for flight-critical systems Challenges of sound static analysis IKOS: an open architecture for sound static analyzers Applications of IKOS
IKOS: Flexible Static Analysis Design Inference Kernel for Open Static Analyzers A development platform for building static analyzers Library of C++ classes encapsulating high performance static analysis algorithms A static analyzer is assembled from the building blocks provided by IKOS An effective buffer overflow analyzer for C programs can be written in a few hundred lines of C++ using IKOS
Flexible C/C++ Front-End The untold story of using static analysis tools Getting the code to just parse is a daunting task The front-end of most static analysis tools expects standard C/C++ code as an input, which is rarely the case for embedded software Significant changes to the build/code may be required IKOS is based on the LLVM platform The GCC compiler can compile just about any existing code with little or no change GCC can generate LLVM assembly code
Static Analysis Design with IKOS Analyzer Interval Domain Octagon Domain C/C++ Code Decision Procedure Properties GCC Pointer Analysis Fixpoint Iterator Verifier LLVM Verification Report IKOS
Example void f(double *p, int n) { int i; for (i = 0; i < n; i++) { p[i] = ...; } } ... f(&S[3], 8); ... The analysis discovers program properties: 0 i 7 p points to fourth element of structure S
Example void f(double *p, int n) { int i; for (i = 0; i < n; i++) { p[i] = ...; } } Access within bounds? ... f(&S[3], 8); ... The verification uses the properties discovered: Array-bound compliance Check that structure S has at least 11 elements
Specialization of the Analyzer Specialization consists of finding the right blend of algorithms To compute strong enough properties for the verifier And guarantee reasonable analysis times This is an intrinsically empirical process IKOS allows the analysis designer to easily swap abstractions and decision procedures IKOS helps streamline the design of specialized static analyzers
Roadmap Static analysis for flight-critical systems Challenges of sound static analysis IKOS: an open architecture for sound static analyzers Applications of IKOS
Verification of UAS Autopilots Certifying the flight software of unmanned aircrafts is critical for NextGen Complex code bases Variety of platforms and architectures No standard development process like DO178 Static analysis can help Formal verification provides high assurance Cost-effective, works on the code as is
Experiments with IKOS Verification of array-bound compliance (NASA APG milestone) Benchmark of realistic UAS autopilots Juliet is a cyber-security benchmark from NIST and is listed here just to demonstrate the scalability of the analyzer
MATLAB/Simulink Autocode Auto-generated code from MATLAB/Simulink models is increasingly used in critical flight software Static analysis can provide formal guarantees that the autocode satisfies critical safety properties We are currently developing a specialized analyzer for this class of code using IKOS
Technical Infusion Ongoing activities to transfer the technology into NASA missions
Conclusion Static analysis is an important tool for the assurance of flight-critical software There is no silver bullet: static analyzers need to be specialized to be effective IKOS is a step toward streamlining the design of specialized high-performance static analyzers
