nach oben

Erschienen in:

2015 | OriginalPaper | Buchkapitel

Source-Code-to-Object-Code Traceability Analysis for Avionics Software: Don’t Trust Your Compiler

verfasst von : Jörg Brauer, Markus Dahlweid, Tobias Pankrath, Jan Peleska

Erschienen in: Computer Safety, Reliability, and Security

Verlag: Springer International Publishing

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config

KI-gestützte Suche

Aus

Abstract

One objective of structural coverage analysis according to RTCA DO-178C for avionic software of development assurance level A (DAL-A) is to either identify object code that was not exercised during testing, or to provide evidence that all code has been tested in an adequate way. Therefore comprehensive tracing information from source code to object code is required, which is typically derived using a manual source-code-to-object-code (STO) traceability analysis. This paper presents a set of techniques to perform automatic STO traceability analysis using abstract interpretation, which we have implemented in a tool-suite called Rtt-Sto. At its core, the tool tries to prove that the control flow graphs of the object code and the source are isomorphic. Further analyses, such as memory allocation analysis and store analysis are then performed on top. Our approach has been applied during low-level verification for DAL-A avionics software, where the effort for STO analysis was significantly reduced due to a high degree of automation. Importantly, the associated analysis process was accepted by the responsible certification authorities.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Vorheriges Kapitel A Comprehensive Safety, Security, and Serviceability Assessment Method

Nächstes Kapitel Automated Generation of Buffer Overflow Quick Fixes Using Symbolic Execution and SMT

In this paper, the term source code is used to denote code written in a high-level programming language, such as Ada or C/C++.

The latter objective addresses the problem that formally correct code may produce errors at runtime due to hardware/software incompatibilities, such as insufficient register sizes for certain arithmetic operations.

For software of criticality level DAL-C, the standard requires statement coverage, for DAL-B software decision coverage has to be achieved, and MC/DC coverage is required for DAL-A [19, Table A-7].

STO traceability analysis was already required for DAL-A software by the DO-178B [22]. However, the text has often been misunderstood, and clarifications have been published [7, 8]. These clarifications have been incorporated into the DO-178C, which now explicitly mentions that STO traceability not only involves the branching structure of the program, but also the identification of untraceable side-effects in linear code blocks, such as memory accesses or function invocations.

For example, the compiler may call built-in library functions for fast memory copy or for arithmetic operations; these function calls are invisible on source code level.

Think of a switch statement containing all possible switch cases and an additional (superfluous) default-branch.

The compiler tracks the contents of registers to avoid reloading values if they are used again soon. Variables, constants, and structure references such as (a.b) are tracked through linear code blocks.

Move/load/store/branch operations may be re-grouped by the compiler in order to optimise the parallelisation options offered by the RISC processor.

Soundness means that no untraceable object code remains undetected.

CFG reconstruction from source code and object code is not the scope of the paper, and we thus assume that CFGs for both representations are readily available; see Sect. 5 for further details on this issue.

In the example, nodes are labelled with their line numbers from the listing. However, the choice of a labelling is inconsequential as long as the node labels are unique.

Balakrishnan, G., Reps, T.W.: WYSINWYX: what you see is not what you execute. ACM Trans. Program. Lang. Syst. 32(6), 23:1–23:84 (2010)CrossRef

Bardin, S., Baufreton, P., Cornuet, N., Herrmann, P., Labbé, S.: Binary-level testing of embedded programs. In: QSIC, pp. 11–20. IEEE (2013)

Bardin, S., Herrmann, P., Védrine, F.: Refinement-based CFG reconstruction from unstructured programs. In: Jhala, R., Schmidt, D. (eds.) VMCAI 2011. LNCS, vol. 6538, pp. 54–69. Springer, Heidelberg (2011) CrossRef

Bartholomew, D.: Qemu: a multihost, multitarget emulator. Linux J. 2006(145), 3 (2006)

Bordin, M., Comar, C., Gingold, T., Guitton, J., Hainque, O., Quinot, T.: Object and source coverage for critical applications with the couverture open analysis framework. In: ERTS (2010)

Brauer, J., Noll, T., Schlich, B.: Interval analysis of microcontroller code using abstract interpretation of hardware and software. In: SCOPES. ACM (2010)

Certification Authorities Software Team (CAST): Guidelines for Approving Source Code to Object Code Traceability - Position Paper CAST-12. CAST (2002)

Certification Authorities Software Team (CAST): Structural Coverage of Object Code - Position Paper CAST-17. CAST (2003)

Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: POPL, pp. 238–252. ACM (1977)

10.

Dullien, T., Rolles, R.: Graph-based comparison of executable objects. SSTIC 5, 1–13 (2005)

11.

Flake, H.: Structural comparison of executable objects (2004)

12.

Flexeder, A., Petter, M., Seidl, H.: Side-effect analysis of assembly code. In: Yahav, E. (ed.) SAS 2011. LNCS, vol. 6887, pp. 77–94. Springer, Heidelberg (2011) CrossRef

13.

Gao, D., Reiter, M.K., Song, D.: BinHunt: automatically finding semantic differences in binary programs. In: Chen, L., Ryan, M.D., Wang, G. (eds.) ICICS 2008. LNCS, vol. 5308, pp. 238–255. Springer, Heidelberg (2008) CrossRef

14.

Hopcroft, J.: An n log n algorithm for minimizing states in a finite automaton. Technical report, DTIC Document (1971)

15.

Kinder, J., Zuleger, F., Veith, H.: An abstract interpretation-based framework for control flow reconstruction from binaries. In: Jones, N.D., Müller-Olm, M. (eds.) VMCAI 2009. LNCS, vol. 5403, pp. 214–228. Springer, Heidelberg (2009) CrossRef

16.

Leroy, X.: Formal verification of a realistic compiler. Commun. ACM 52(7), 107–115 (2009)CrossRef

17.

Reinbacher, T., Brauer, J.: Precise control flow reconstruction using boolean logic. In: EMSOFT, pp. 117–126. ACM (2011)

18.

Rierson, A.: Developing Safety-Critical Software. CRC Press, Boca Raton (2013)

19.

RTCA SC-205/EUROCAE WG-71: Software Considerations in Airborne Systems and Equipment Certification. No. RTCA DO-178C, RTCA Inc. 1140 Connecticut Avenue, N.W., Suite 1020, Washington, D.C., 20036, December 2011

20.

RTCA SC-205/EUROCAE WG-71: Software Tool Qualification Considerations. No. RTCA DO-330, RTCA, Inc., December 2011

21.

RTCA SC-205/EUROCAE WG-71: Supporting Information for DO-178C and DO-278A. No. RTCA DO-248C, RTCA, Inc., December 2011

22.

RTCA, SC-167: Software Considerations in Airborne Systems and Equipment Certification, RTCA/DO-178B. RTCA (1992)

23.

European Committee for Electrotechnical Standardization: EN 50128:2011 - Railway applications - Communications, signalling and processing systems - Software for railway control and protection systems. CENELEC, Brussels (2001)

24.

Sobek, S.,Burke, K.: Power PC Embedded Application Binary Interface (EABI): 32-Bit Implementation. Freescale Semiconductor Inc. (2004)

Titel: Source-Code-to-Object-Code Traceability Analysis for Avionics Software: Don’t Trust Your Compiler
verfasst von: Jörg Brauer
Markus Dahlweid
Tobias Pankrath
Jan Peleska
Verlag: Springer International Publishing
Buch: Computer Safety, Reliability, and Security
Print ISBN: 978-3-319-24254-5

Electronic ISBN: 978-3-319-24255-2

Copyright-Jahr: 2015
DOI: https://doi.org/10.1007/978-3-319-24255-2_31

Springer Professional

Abstract

Bitte loggen Sie sich ein, um Zugang zu Ihrer Lizenz zu erhalten.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"