Some Assembly Required - Program Analysis of Embedded System Code

Ansgar Fehnker, Ralf Huuck, Felix Rauch, Sean Seefried

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

3 Citations (Scopus)

Abstract

Programming embedded system software typically involves more than one programming language. Normally, a high-level language such as C/C++ is used for application oriented tasks and a low-level assembly language for direct interaction with the underlying hardware. In most cases those languages are closely interwoven and the assembly is embedded in the C/C++ code. Verification of such programs requires the integrated analysis of both languages at the same time. However, common algorithmic verification tools fail to address this issue. In this work we present a model-checking based static analysis approach which seamlessly integrates the analysis of embedded ARM assembly with C/C++ code analysis. In particular, we show how to automatically check that the ARM code complies to its interface descriptions. Given interface compliance, we then provide an extended analysis framework for checking general properties of ARM code. We implemented this analysis in our source code analysis tool Goanna, and applied to the source code of an L4 micro kernel implementation.
Original languageEnglish
Title of host publicationEighth IEEE International Working Conference on Source Code Analysis and Manipulation (SCAM 2008)
PublisherIEEE Computer Society
Pages15-24
Number of pages10
ISBN (Print)978-0-7695-3353-7
DOIs
Publication statusPublished - 2008
Externally publishedYes
EventEighth IEEE International Working Conference on Source Code Analysis and Manipulation - Beijing Friendship Hotel, Beijing, China
Duration: 28 Sep 200829 Sep 2008
Conference number: 8
http://www.ieee-scam.org/2008/

Conference

ConferenceEighth IEEE International Working Conference on Source Code Analysis and Manipulation
Abbreviated titleSCAM 2008
CountryChina
CityBeijing
Period28/09/0829/09/08
Internet address

Fingerprint

Program assemblers
Embedded systems
High level languages
Model checking
Static analysis
Computer programming
Computer programming languages
Hardware

Cite this

Fehnker, A., Huuck, R., Rauch, F., & Seefried, S. (2008). Some Assembly Required - Program Analysis of Embedded System Code. In Eighth IEEE International Working Conference on Source Code Analysis and Manipulation (SCAM 2008) (pp. 15-24). IEEE Computer Society. https://doi.org/10.1109/SCAM.2008.15
Fehnker, Ansgar ; Huuck, Ralf ; Rauch, Felix ; Seefried, Sean. / Some Assembly Required - Program Analysis of Embedded System Code. Eighth IEEE International Working Conference on Source Code Analysis and Manipulation (SCAM 2008). IEEE Computer Society, 2008. pp. 15-24
@inproceedings{6de2819e9af24efeb1505ce4205adadf,
title = "Some Assembly Required - Program Analysis of Embedded System Code",
abstract = "Programming embedded system software typically involves more than one programming language. Normally, a high-level language such as C/C++ is used for application oriented tasks and a low-level assembly language for direct interaction with the underlying hardware. In most cases those languages are closely interwoven and the assembly is embedded in the C/C++ code. Verification of such programs requires the integrated analysis of both languages at the same time. However, common algorithmic verification tools fail to address this issue. In this work we present a model-checking based static analysis approach which seamlessly integrates the analysis of embedded ARM assembly with C/C++ code analysis. In particular, we show how to automatically check that the ARM code complies to its interface descriptions. Given interface compliance, we then provide an extended analysis framework for checking general properties of ARM code. We implemented this analysis in our source code analysis tool Goanna, and applied to the source code of an L4 micro kernel implementation.",
author = "Ansgar Fehnker and Ralf Huuck and Felix Rauch and Sean Seefried",
year = "2008",
doi = "10.1109/SCAM.2008.15",
language = "English",
isbn = "978-0-7695-3353-7",
pages = "15--24",
booktitle = "Eighth IEEE International Working Conference on Source Code Analysis and Manipulation (SCAM 2008)",
publisher = "IEEE Computer Society",
address = "United States",

}

Fehnker, A, Huuck, R, Rauch, F & Seefried, S 2008, Some Assembly Required - Program Analysis of Embedded System Code. in Eighth IEEE International Working Conference on Source Code Analysis and Manipulation (SCAM 2008). IEEE Computer Society, pp. 15-24, Eighth IEEE International Working Conference on Source Code Analysis and Manipulation, Beijing, China, 28/09/08. https://doi.org/10.1109/SCAM.2008.15

Some Assembly Required - Program Analysis of Embedded System Code. / Fehnker, Ansgar; Huuck, Ralf; Rauch, Felix; Seefried, Sean.

Eighth IEEE International Working Conference on Source Code Analysis and Manipulation (SCAM 2008). IEEE Computer Society, 2008. p. 15-24.

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

TY - GEN

T1 - Some Assembly Required - Program Analysis of Embedded System Code

AU - Fehnker, Ansgar

AU - Huuck, Ralf

AU - Rauch, Felix

AU - Seefried, Sean

PY - 2008

Y1 - 2008

N2 - Programming embedded system software typically involves more than one programming language. Normally, a high-level language such as C/C++ is used for application oriented tasks and a low-level assembly language for direct interaction with the underlying hardware. In most cases those languages are closely interwoven and the assembly is embedded in the C/C++ code. Verification of such programs requires the integrated analysis of both languages at the same time. However, common algorithmic verification tools fail to address this issue. In this work we present a model-checking based static analysis approach which seamlessly integrates the analysis of embedded ARM assembly with C/C++ code analysis. In particular, we show how to automatically check that the ARM code complies to its interface descriptions. Given interface compliance, we then provide an extended analysis framework for checking general properties of ARM code. We implemented this analysis in our source code analysis tool Goanna, and applied to the source code of an L4 micro kernel implementation.

AB - Programming embedded system software typically involves more than one programming language. Normally, a high-level language such as C/C++ is used for application oriented tasks and a low-level assembly language for direct interaction with the underlying hardware. In most cases those languages are closely interwoven and the assembly is embedded in the C/C++ code. Verification of such programs requires the integrated analysis of both languages at the same time. However, common algorithmic verification tools fail to address this issue. In this work we present a model-checking based static analysis approach which seamlessly integrates the analysis of embedded ARM assembly with C/C++ code analysis. In particular, we show how to automatically check that the ARM code complies to its interface descriptions. Given interface compliance, we then provide an extended analysis framework for checking general properties of ARM code. We implemented this analysis in our source code analysis tool Goanna, and applied to the source code of an L4 micro kernel implementation.

U2 - 10.1109/SCAM.2008.15

DO - 10.1109/SCAM.2008.15

M3 - Conference contribution

SN - 978-0-7695-3353-7

SP - 15

EP - 24

BT - Eighth IEEE International Working Conference on Source Code Analysis and Manipulation (SCAM 2008)

PB - IEEE Computer Society

ER -

Fehnker A, Huuck R, Rauch F, Seefried S. Some Assembly Required - Program Analysis of Embedded System Code. In Eighth IEEE International Working Conference on Source Code Analysis and Manipulation (SCAM 2008). IEEE Computer Society. 2008. p. 15-24 https://doi.org/10.1109/SCAM.2008.15