More Web Proxy on the site http://driver.im/

research-article

Interval analysis of microcontroller code using abstract interpretation of hardware and software

Authors:

Bastian SchlichAuthors Info & Claims

SCOPES '10: Proceedings of the 13th International Workshop on Software & Compilers for Embedded Systems

Article No.: 3, Pages 1 - 10

https://doi.org/10.1145/1811212.1811216

Published: 28 June 2010 Publication History

Abstract

Static analysis is often performed on source code where intervals -- possibly the most widely used numeric abstract domain -- have successfully been used as a program abstraction for decades. Binary code on microcontroller platforms, however, is different from high-level code in that data is frequently altered using bitwise operations and the results of operations often depend on the hardware configuration. We describe a method that combines word- and bit-level interval analysis and integrates a hardware model by means of abstract interpretation in order to handle these peculiarities. Moreover, we show that this method proves powerful enough to derive invariants that could so far only be verified using computationally more expensive techniques such as model checking.

References

[1]

Atmel Corp. 8-bit AVR Instruction Set, July 2008.

[2]

G. Balakrishnan, T. W. Reps, D. Melski, and T. Teitelbaum. WYSINWYX: What you see is not what you execute. In VSTTE 05, volume 4171 of LNCS, pages 202--213. Springer, 2005.

[3]

S. Bardin and P. Herrmann. Structural testing of executables. In ICST 08, pages 240--249. IEEE, 2008.

Digital Library

[4]

S. Bardin, P. Herrmann, and F. Perroud. An alternative to SAT-based approaches for bit-vectors. In TACAS 2010, volume 6015 of LNCS. Springer, 2010.

Digital Library

[5]

L. Chen, A. Mine, J. Wang, and P. Cousot. Interval polyhedra: An abstract domain to infer interval linear relationships. In SAS 2009, volume 5673 of LNCS, pages 309--325. Springer, 2009.

Digital Library

[6]

C. Cifuentes and A. Fraboulet. Intraprocedural static slicing of binary executables. In ICSM 97, pages 188--195. IEEE, 1997.

Digital Library

[7]

P. Cousot and R. Cousot. Static determination of dynamic properties of programs. In Proc. of the 2nd International Symposium on Programming, pages 106--130. Dunod, Paris, France, 1976.

[8]

P. Cousot and R. Cousot. Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In POPL 77, pages 238--252. ACM, 1977.

Digital Library

[9]

P. Cousot and R. Cousot. Comparing the Galois connection and widening/narrowing approaches to abstract interpretation. In PLILP 92, volume 631 of LNCS, pages 269--295. Springer, 1992.

Digital Library

[10]

P. Cousot, R. Cousot, J. Feret, L. Mauborgne, A. Mine, D. Monniaux, and X. Rival. The Astrée analyser. In ESOP 05, volume 3444 of LNCS, pages 21--30. Springer, 2005.

Digital Library

[11]

S. Debray, R. Muth, and M. Weippert. Alias analysis of executable code. In POPL 98, pages 12--24. ACM, 1998.

Digital Library

[12]

A. Fehnker, R. Huuck, and S. Seefried. Incremental false path elimination for static software analysis. In ATVA 09, volume 5799 of LNCS, pages 255--270. Springer, 2009.

Digital Library

[13]

T. Gawlitza, J. Leroux, J. Reineke, H. Seidl, G. Sutre, and R. Wilhelm. Polynomial precise interval analysis revisited. In Efficient Algorithms, volume 5760 of LNCS, pages 422--437. Springer, 2009.

Digital Library

[14]

B. Guo, M. Bridges, S. Triantafyllis, G. Ottoni, E. Raman, and D. August. Practical and accurate low-level pointer analysis. In CGO 05, pages 291--302. IEEE, 2005.

Digital Library

[15]

M. Hind and A. Pioli. Assessing the effects of flow-sensitivity on pointer alias analyses. In SAS 98, LNCS, pages 57--81. Springer, 1998.

Digital Library

[16]

S. Horwitz, T. Reps, and D. Binkley. Interprocedural slicing using dependence graphs. ACM Trans. Program. Lang. Syst., 12(1):26--60, January 1990.

Digital Library

[17]

J. Howe and A. King. Logahedra: A new weakly relational domain. In ATVA 09, LNCS. Springer, 2009.

Digital Library

[18]

F. Ivancic, Z. Yang, M. Ganai, A. Gupta, I. Shlyakhter, and P. Ashar. F-Soft: Software verification platform. In CAV 05, volume 3576 of LNCS, pages 301--306. Springer, 2005.

Digital Library

[19]

M. Karr. Affine relationships among variables of a program. Acta Informatica, 6:133--151, 1976.

Digital Library

[20]

J. Kinder, H. Veith, and F. Zuleger. An abstract interpretation-based framework for control flow reconstruction from binaries. In VMCAI 09, volume 5403 of LNCS, pages 214--228. Springer, 2009.

Digital Library

[21]

A. King and H. Søndergaard. Automatic abstraction for congruences. In VMCAI 10, volume 5944 of LNCS, pages 197--213. Springer, 2010.

Digital Library

[22]

M. Müller-Olm and H. Seidl. Analysis of modular arithmetic. ACM Trans. Program. Lang. Syst., 29(5), August 2007.

Digital Library

[23]

D. J. Pearce, P. H. J. Kelly, and C. Hankin. Efficient field-sensitive pointer analysis of C. ACM Trans. Program. Lang. Syst., 30(1), 2007.

Digital Library

[24]

J. Regehr, A. Reid, and K. Webb. Eliminating stack overflow by abstract interpretation. In EMSOFT 03, pages 306--322, 2003.

[25]

T. W. Reps and G. Balakrishnan. Improved memory-access analysis for x86 executables. In CC 08, volume 4959 of LNCS, pages 16--35. Springer, 2008.

Digital Library

[26]

B. Schlich. Model Checking of Software for Microcontrollers. Dissertation, RWTH Aachen University, Aachen, Germany, June 2008.

[27]

B. Schlich, T. Noll, J. Brauer, and L. Brutschy. Reduction of interrupt handler executions for model checking embedded software. In HVC 2009, LNCS. Springer, 2009. To appear.

Digital Library

[28]

R. Tarjan. Depth-first search and linear graph algorithms. SIAM Journal on Computing, 1(2):146--160, 1972.

[29]

X. Yang, N. Cooprider, and J. Regehr. Eliminating the call stack to save ram. In LCTES 09. ACM Press, 2009. To appear.

Digital Library

[30]

K. Yorav and O. Grumberg. Static analysis for state-space reductions preserving temporal logics. Formal Methods in System Design, 25(1):67--96, 2004.

Digital Library

Cited By

Yu SLiu ZWang TWang J(2024)Neural Solving Uninterpreted Predicates with Abstract Gradient DescentACM Transactions on Software Engineering and Methodology10.1145/367539433:8(1-47)Online publication date: 2-Jul-2024
https://dl.acm.org/doi/10.1145/3675394
Küchler AWenning LWendland F(2023)AbsIntIO: Towards Showing the Absence of Integer Overflows in Binaries using Abstract InterpretationProceedings of the 2023 ACM Asia Conference on Computer and Communications Security10.1145/3579856.3582814(247-258)Online publication date: 10-Jul-2023
https://dl.acm.org/doi/10.1145/3579856.3582814
Brauer J(2023)Source-Code-to-Object-Code Traceability Analysis for Airborne Software: A Case for Tool SupportApplicable Formal Methods for Safe Industrial Products10.1007/978-3-031-40132-9_16(257-271)Online publication date: 17-Aug-2023
https://doi.org/10.1007/978-3-031-40132-9_16
Show More Cited By

Index Terms

Interval analysis of microcontroller code using abstract interpretation of hardware and software
1. Software and its engineering
  1. Software creation and management
    1. Software verification and validation
      1. Formal software verification
  2. Software organization and properties
    1. Software functional properties
      1. Formal methods
2. Theory of computation
  1. Semantics and reasoning
    1. Program reasoning
      1. Program analysis
      2. Program verification
    2. Program semantics

Recommendations

Static analysis by abstract interpretation of embedded critical software

Formal methods are increasingly used to help ensuring the correctness of complex, critical embedded software systems. We show how sound semantic static analyses based on Abstract Interpretation may be used to check properties at various levels of a ...
Pushdown control-flow analysis for free
POPL '16

Traditional control-flow analysis (CFA) for higher-order languages introduces spurious connections between callers and callees, and different invocations of a function may pollute each other's return flows. Recently, three distinct approaches have been ...
Static program analysis of embedded executable assembly code
CASES '04: Proceedings of the 2004 international conference on Compilers, architecture, and synthesis for embedded systems

We consider the problem of automatically checking if coding standards have been followed in the development of embedded applications. The problem arises from practical considerations because DSP chip manufacturers (in our case Texas Instruments) want ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Other conferences

SCOPES '10: Proceedings of the 13th International Workshop on Software & Compilers for Embedded Systems

June 2010

91 pages

ISBN:9781450300841

DOI:10.1145/1811212

General Chair:
Ed Deprettere
Leiden University, NL
,
Program Chair:
Todor Stefanov
Leiden University, NL

Copyright © 2010 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Sponsors

EDAA: European Design Automation Association

In-Cooperation

SIGBED: ACM Special Interest Group on Embedded Systems

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 28 June 2010

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Conference

SCOPES '10

Sponsor:

EDAA

SCOPES '10: 13th International Workshop on Software and Compilers for Embedded Systems

June 28 - 29, 2010

St. Goar, Germany

Acceptance Rates

Overall Acceptance Rate 38 of 79 submissions, 48%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

12
Total Citations
View Citations
236
Total Downloads

Downloads (Last 12 months)11
Downloads (Last 6 weeks)2

Reflects downloads up to 12 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

Yu SLiu ZWang TWang J(2024)Neural Solving Uninterpreted Predicates with Abstract Gradient DescentACM Transactions on Software Engineering and Methodology10.1145/367539433:8(1-47)Online publication date: 2-Jul-2024
https://dl.acm.org/doi/10.1145/3675394
Küchler AWenning LWendland F(2023)AbsIntIO: Towards Showing the Absence of Integer Overflows in Binaries using Abstract InterpretationProceedings of the 2023 ACM Asia Conference on Computer and Communications Security10.1145/3579856.3582814(247-258)Online publication date: 10-Jul-2023
https://dl.acm.org/doi/10.1145/3579856.3582814
Brauer J(2023)Source-Code-to-Object-Code Traceability Analysis for Airborne Software: A Case for Tool SupportApplicable Formal Methods for Safe Industrial Products10.1007/978-3-031-40132-9_16(257-271)Online publication date: 17-Aug-2023
https://doi.org/10.1007/978-3-031-40132-9_16
Herber PLiebrenz T(2020)Dependence Analysis and Automated Partitioning for Scalable Formal Analysis of SystemC Designs2020 18th ACM-IEEE International Conference on Formal Methods and Models for System Design (MEMOCODE)10.1109/MEMOCODE51338.2020.9314998(1-6)Online publication date: 2-Dec-2020
https://doi.org/10.1109/MEMOCODE51338.2020.9314998
Toman JGrossman D(2019)Concerto: a framework for combined concrete and abstract interpretationProceedings of the ACM on Programming Languages10.1145/32903563:POPL(1-29)Online publication date: 2-Jan-2019
https://dl.acm.org/doi/10.1145/3290356
Brauer JDahlweid MPeleska J(2015)Tool-Supported Structural Coverage Analysis for DO-178C Compliant SoftwareSAE Technical Paper Series10.4271/2015-01-2558Online publication date: 15-Sep-2015
https://doi.org/10.4271/2015-01-2558
Brauer JDahlweid MPankrath TPeleska J(2015)Source-Code-to-Object-Code Traceability Analysis for Avionics SoftwareProceedings of the 34th International Conference on Computer Safety, Reliability, and Security - Volume 933710.1007/978-3-319-24255-2_31(427-440)Online publication date: 23-Sep-2015
https://dl.acm.org/doi/10.1007/978-3-319-24255-2_31
Herber P(2014)The RESCUE Approach - Towards Compositional Hardware/Software Co-verificationProceedings of the 2014 IEEE Intl Conf on High Performance Computing and Communications, 2014 IEEE 6th Intl Symp on Cyberspace Safety and Security, 2014 IEEE 11th Intl Conf on Embedded Software and Syst (HPCC,CSS,ICESS)10.1109/HPCC.2014.109(721-724)Online publication date: 20-Aug-2014
https://dl.acm.org/doi/10.1109/HPCC.2014.109
Reinbacher TBrauer JChakraborty SJerraya ABaruah SFischmeister S(2011)Precise control flow reconstruction using boolean logicProceedings of the ninth ACM international conference on Embedded software10.1145/2038642.2038662(117-126)Online publication date: 9-Oct-2011
https://dl.acm.org/doi/10.1145/2038642.2038662
Beckschulze EBrauer JStollenwerk AKowalewski S(2011)Analyzing Embedded Systems Code for Mixed-Critical Systems Using Hybrid Memory RepresentationsProceedings of the 2011 14th IEEE International Symposium on Object/Component/Service-Oriented Real-Time Distributed Computing Workshops10.1109/ISORCW.2011.40(33-40)Online publication date: 28-Mar-2011
https://dl.acm.org/doi/10.1109/ISORCW.2011.40
Show More Cited By

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Table of Contents