Tempel, 2024 - Google Patents
Accurate binary-level symbolic execution of embedded firmwareTempel, 2024
View PDF- Document ID
- 11420456506687984279
- Author
- Tempel S
- Publication year
External Links
Snippet
Symbolic execution is an automated software testing technique that has enabled the discovery of numerous bugs in conventional, non-embedded software. Unfortunately, its application to embedded firmware is presently limited due to unique challenges associated …
- 230000002093 peripheral effect 0 abstract description 158
Classifications
-
- G—PHYSICS
- G06—COMPUTING; CALCULATING; COUNTING
- G06F—ELECTRICAL DIGITAL DATA PROCESSING
- G06F11/00—Error detection; Error correction; Monitoring
- G06F11/36—Preventing errors by testing or debugging software
- G06F11/362—Software debugging
- G06F11/3648—Software debugging using additional hardware
- G06F11/3656—Software debugging using additional hardware using a specific debug interface
-
- G—PHYSICS
- G06—COMPUTING; CALCULATING; COUNTING
- G06F—ELECTRICAL DIGITAL DATA PROCESSING
- G06F11/00—Error detection; Error correction; Monitoring
- G06F11/36—Preventing errors by testing or debugging software
- G06F11/362—Software debugging
- G06F11/3636—Software debugging by tracing the execution of the program
-
- G—PHYSICS
- G06—COMPUTING; CALCULATING; COUNTING
- G06F—ELECTRICAL DIGITAL DATA PROCESSING
- G06F11/00—Error detection; Error correction; Monitoring
- G06F11/36—Preventing errors by testing or debugging software
- G06F11/3668—Software testing
- G06F11/3672—Test management
- G06F11/3688—Test management for test execution, e.g. scheduling of test suites
-
- G—PHYSICS
- G06—COMPUTING; CALCULATING; COUNTING
- G06F—ELECTRICAL DIGITAL DATA PROCESSING
- G06F17/00—Digital computing or data processing equipment or methods, specially adapted for specific functions
- G06F17/50—Computer-aided design
- G06F17/5009—Computer-aided design using simulation
- G06F17/504—Formal methods
-
- G—PHYSICS
- G06—COMPUTING; CALCULATING; COUNTING
- G06F—ELECTRICAL DIGITAL DATA PROCESSING
- G06F9/00—Arrangements for programme control, e.g. control unit
- G06F9/06—Arrangements for programme control, e.g. control unit using stored programme, i.e. using internal store of processing equipment to receive and retain programme
- G06F9/44—Arrangements for executing specific programmes
- G06F9/455—Emulation; Software simulation, i.e. virtualisation or emulation of application or operating system execution engines
-
- G—PHYSICS
- G06—COMPUTING; CALCULATING; COUNTING
- G06F—ELECTRICAL DIGITAL DATA PROCESSING
- G06F17/00—Digital computing or data processing equipment or methods, specially adapted for specific functions
- G06F17/50—Computer-aided design
- G06F17/5009—Computer-aided design using simulation
- G06F17/5022—Logic simulation, e.g. for logic circuit operation
-
- G—PHYSICS
- G06—COMPUTING; CALCULATING; COUNTING
- G06F—ELECTRICAL DIGITAL DATA PROCESSING
- G06F11/00—Error detection; Error correction; Monitoring
- G06F11/36—Preventing errors by testing or debugging software
- G06F11/362—Software debugging
- G06F11/3632—Software debugging of specific synchronisation aspects
-
- G—PHYSICS
- G06—COMPUTING; CALCULATING; COUNTING
- G06F—ELECTRICAL DIGITAL DATA PROCESSING
- G06F11/00—Error detection; Error correction; Monitoring
- G06F11/22—Detection or location of defective computer hardware by testing during standby operation or during idle time, e.g. start-up testing
- G06F11/26—Functional testing
- G06F11/261—Functional testing by simulating additional hardware, e.g. fault simulation
-
- G—PHYSICS
- G06—COMPUTING; CALCULATING; COUNTING
- G06F—ELECTRICAL DIGITAL DATA PROCESSING
- G06F11/00—Error detection; Error correction; Monitoring
- G06F11/30—Monitoring
- G06F11/34—Recording or statistical evaluation of computer activity, e.g. of down time, of input/output operation; Recording or statistical evaluation of user activity, e.g. usability assessment
- G06F11/3466—Performance evaluation by tracing or monitoring
-
- G—PHYSICS
- G06—COMPUTING; CALCULATING; COUNTING
- G06F—ELECTRICAL DIGITAL DATA PROCESSING
- G06F11/00—Error detection; Error correction; Monitoring
- G06F11/22—Detection or location of defective computer hardware by testing during standby operation or during idle time, e.g. start-up testing
- G06F11/26—Functional testing
- G06F11/27—Built-in tests
-
- G—PHYSICS
- G06—COMPUTING; CALCULATING; COUNTING
- G06F—ELECTRICAL DIGITAL DATA PROCESSING
- G06F11/00—Error detection; Error correction; Monitoring
- G06F11/36—Preventing errors by testing or debugging software
- G06F11/3664—Environments for testing or debugging software
-
- G—PHYSICS
- G06—COMPUTING; CALCULATING; COUNTING
- G06F—ELECTRICAL DIGITAL DATA PROCESSING
- G06F8/00—Arrangements for software engineering
- G06F8/40—Transformations of program code
-
- G—PHYSICS
- G06—COMPUTING; CALCULATING; COUNTING
- G06F—ELECTRICAL DIGITAL DATA PROCESSING
- G06F21/00—Security arrangements for protecting computers, components thereof, programs or data against unauthorised activity
-
- G—PHYSICS
- G06—COMPUTING; CALCULATING; COUNTING
- G06F—ELECTRICAL DIGITAL DATA PROCESSING
- G06F2201/00—Indexing scheme relating to error detection, to error correction, and to monitoring
-
- G—PHYSICS
- G06—COMPUTING; CALCULATING; COUNTING
- G06F—ELECTRICAL DIGITAL DATA PROCESSING
- G06F2217/00—Indexing scheme relating to computer aided design [CAD]
- G06F2217/86—Hardware-Software co-design
-
- G—PHYSICS
- G06—COMPUTING; CALCULATING; COUNTING
- G06F—ELECTRICAL DIGITAL DATA PROCESSING
- G06F15/00—Digital computers in general; Data processing equipment in general
Similar Documents
| Publication | Publication Date | Title |
|---|---|---|
| Fasano et al. | Sok: Enabling security analyses of embedded systems via rehosting | |
| Huang et al. | Instruction-level abstraction (ila) a uniform specification for system-on-chip (soc) verification | |
| Dasgupta et al. | A complete formal semantics of x86-64 user-level instruction set architecture | |
| Herdt et al. | Enhanced Virtual Prototyping | |
| US20110307688A1 (en) | Synthesis system for pipelined digital circuits | |
| Tempel et al. | SymEx-VP: An open source virtual prototype for OS-agnostic concolic testing of IoT firmware | |
| Dobis et al. | Verification of chisel hardware designs with chiselverify | |
| Herdt et al. | Advanced virtual prototyping for cyber-physical systems using RISC-V: implementation, verification and challenges | |
| Herdt et al. | Verification of embedded binaries using coverage-guided fuzzing with systemc-based virtual prototypes | |
| Renner et al. | A hardware in the loop benchmark suite to evaluate NIST LWC ciphers on microcontrollers | |
| Chen et al. | End-to-end concolic testing for hardware/software co-validation | |
| Joannou et al. | Randomized testing of RISC-V CPUs using direct instruction injection | |
| Villarraga et al. | Software in a Hardware View: New Models for HW-dependent Software in SoC Verification | |
| Lugou et al. | Toward a methodology for unified verification of hardware/software co-designs | |
| Wicaksana et al. | Virtual prototyping platform for multiprocessor system-on-chip hardware/software co-design and co-verification | |
| Tempel et al. | Automated detection of spatial memory safety violations for constrained devices | |
| Tempel | Accurate binary-level symbolic execution of embedded firmware | |
| Charvát et al. | Automatic formal correspondence checking of ISA and RTL microprocessor description | |
| Gilani | Methodologies for Accelerated Open-Source Hardware Verification and Optimization | |
| Nataraja | A Research-Fertile Co-Emulation Framework for RISC-V Processor Verification | |
| Deutschbein | Mining Secure Behavior of Hardware Designs | |
| Tain et al. | Survey of Verification of RISC-V Processors | |
| Alam et al. | Virsoc: Automatic synthesis of virtual system-on-chip environments | |
| Forcioli | Modeling of micro-architecture for security with gem5 | |
| Mysore Nataraja | A Research-Fertile Co-Emulation Framework for RISC-V Processor Verification |