Range Analysis of Microcontroller Code Using Bit-Level Congruences

被引:0
|
作者
Brauer, Joerg [1 ]
King, Andy [2 ]
Kowalewski, Stefan [1 ]
机构
[1] Rhein Westfal TH Aachen, Embedded Software Lab, Aachen, Germany
[2] Portcullis Comp Secur, London HA5 2EX, England
来源
FORMAL METHODS FOR INDUSTRIAL CRITICAL SYSTEMS | 2010年 / 6371卷
关键词
D O I
暂无
中图分类号
TP31 [计算机软件];
学科分类号
081202 ; 0835 ;
摘要
Bitwise instructions, loops and indirect data access pose difficult challenges to the verification of microcontroller programs. In particular, it is necessary to show that an indirect write does not mutate registers, which are indirectly addressable. To prove this property, among others, this paper presents a relational binary-code semantics and details how this can be used to compute program invariants in terms of bit-level congruences. Moreover, it demonstrates how congruences can be combined with intervals to derive accurate ranges, as well as information about strided indirect memory accesses.
引用
收藏
页码:82 / +
页数:3
相关论文
共 50 条
  • [31] A chaotic color image encryption using integrated bit-level permutation
    Teng, Lin
    Wang, Xingyuan
    Meng, Juan
    MULTIMEDIA TOOLS AND APPLICATIONS, 2018, 77 (06) : 6883 - 6896
  • [32] BEC: Bit-Level Static Analysis for Reliability against Soft Errors
    Ko, Yousun
    Burgstaller, Bernd
    2024 IEEE/ACM INTERNATIONAL SYMPOSIUM ON CODE GENERATION AND OPTIMIZATION, CGO, 2024, : 283 - 295
  • [33] Bit-level architectures for Montgomery's multiplication
    Nibouche, O
    Bouridane, A
    Nibouche, M
    ICECS 2001: 8TH IEEE INTERNATIONAL CONFERENCE ON ELECTRONICS, CIRCUITS AND SYSTEMS, VOLS I-III, CONFERENCE PROCEEDINGS, 2001, : 273 - 276
  • [34] Bit-level Perceptron Prediction for Indirect Branches
    Garza, Elba
    Mirbagher, Samira
    Khan, Tahsin Ahmad
    Jimenez, Daniel A.
    PROCEEDINGS OF THE 2019 46TH INTERNATIONAL SYMPOSIUM ON COMPUTER ARCHITECTURE (ISCA '19), 2019, : 27 - 38
  • [35] Fast and Efficient Bit-Level Precision Tuning
    Adje, Assale
    Ben Khalifa, Dorra
    Martel, Matthieu
    STATIC ANALYSIS, SAS 2021, 2021, 12913 : 1 - 24
  • [36] Bit-level scheduling of heterogeneous behavioural specifications
    Molina, MC
    Mendías, JM
    Hermida, R
    IEEE/ACM INTERNATIONAL CONFERENCE ON CAD-02, DIGEST OF TECHNICAL PAPERS, 2002, : 602 - 608
  • [37] Dynamic Reconfiguration of bit-level arithmetic Units
    Pfaender, O. A.
    Pfleiderer, H-J
    ADVANCES IN RADIO SCIENCE, 2005, 3 : 319 - 323
  • [38] Bit-Level Affixation Text Compression Algorithms
    Lewan, Prayat
    Khancome, Chouvalit
    2024 21ST INTERNATIONAL JOINT CONFERENCE ON COMPUTER SCIENCE AND SOFTWARE ENGINEERING, JCSSE 2024, 2024, : 161 - 166
  • [39] A BIT-LEVEL SYSTOLIC IMPLEMENTATION OF THE MEDIAN FILTER
    HU, Z
    KING, GA
    MICROPROCESSORS AND MICROSYSTEMS, 1995, 19 (04) : 185 - 186
  • [40] On Bit-Level Decoding of Nonbinary LDPC Codes
    Zhang, Mu
    Cai, Kui
    Huang, Qin
    Yuan, Shuai
    IEEE TRANSACTIONS ON COMMUNICATIONS, 2018, 66 (09) : 3736 - 3748