Some assembly required: program analysis of embedded system code

Ansgar Fehnker; Ralf Huuck; Felix Rauch; Sean Seefried

doi:10.1109/SCAM.2008.15

Some assembly required: program analysis of embedded system code

Ansgar Fehnker, Ralf Huuck, Felix Rauch, Sean Seefried

Research output: Chapter in Book/Report/Conference proceeding › Conference proceeding contribution › peer-review

10 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 language	English
Title of host publication	Proceedings of Eighth IEEE International Working Conference on Source Code Analysis and Manipulation (SCAM 2008)
Editors	James R. Cordy, Lu Zhang
Place of Publication	Los Alamitos, CA
Publisher	Institute of Electrical and Electronics Engineers (IEEE)
Pages	15-24
Number of pages	10
ISBN (Print)	9780769533537
DOIs	https://doi.org/10.1109/SCAM.2008.15
Publication status	Published - 2008
Externally published	Yes
Event	8th IEEE International Working Conference on Source Code Analysis and Manipulation, SCAM 2008 - Beijing, China Duration: 28 Sept 2008 → 29 Sept 2008

Conference

Conference	8th IEEE International Working Conference on Source Code Analysis and Manipulation, SCAM 2008
Country/Territory	China
City	Beijing
Period	28/09/08 → 29/09/08

Access to Document

10.1109/SCAM.2008.15

Cite this

Fehnker, A., Huuck, R., Rauch, F., & Seefried, S. (2008). Some assembly required: program analysis of embedded system code. In J. R. Cordy, & L. Zhang (Eds.), Proceedings of Eighth IEEE International Working Conference on Source Code Analysis and Manipulation (SCAM 2008) (pp. 15-24). Institute of Electrical and Electronics Engineers (IEEE). https://doi.org/10.1109/SCAM.2008.15

@inproceedings{03f4b1da3e2f4f38bc7b8de92b1873d6,

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 = "9780769533537",

pages = "15--24",

editor = "Cordy, {James R.} and Lu Zhang",

booktitle = "Proceedings of Eighth IEEE International Working Conference on Source Code Analysis and Manipulation (SCAM 2008)",

publisher = "Institute of Electrical and Electronics Engineers (IEEE)",

address = "United States",

note = "8th IEEE International Working Conference on Source Code Analysis and Manipulation, SCAM 2008 ; Conference date: 28-09-2008 Through 29-09-2008",

}

Fehnker, A, Huuck, R, Rauch, F & Seefried, S 2008, Some assembly required: program analysis of embedded system code. in JR Cordy & L Zhang (eds), Proceedings of Eighth IEEE International Working Conference on Source Code Analysis and Manipulation (SCAM 2008). Institute of Electrical and Electronics Engineers (IEEE), Los Alamitos, CA, pp. 15-24, 8th IEEE International Working Conference on Source Code Analysis and Manipulation, SCAM 2008, 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 et al.
Proceedings of Eighth IEEE International Working Conference on Source Code Analysis and Manipulation (SCAM 2008). ed. / James R. Cordy; Lu Zhang. Los Alamitos, CA: Institute of Electrical and Electronics Engineers (IEEE), 2008. p. 15-24.

Research output: Chapter in Book/Report/Conference proceeding › Conference proceeding contribution › peer-review

TY - GEN

T1 - Some assembly required

T2 - 8th IEEE International Working Conference on Source Code Analysis and Manipulation, SCAM 2008

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 proceeding contribution

SN - 9780769533537

SP - 15

EP - 24

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

A2 - Cordy, James R.

A2 - Zhang, Lu

PB - Institute of Electrical and Electronics Engineers (IEEE)

CY - Los Alamitos, CA

Y2 - 28 September 2008 through 29 September 2008

ER -

Some assembly required: program analysis of embedded system code

Abstract

Conference

Access to Document

Fingerprint

Cite this