Formalizing the Execution Semantics of the Armv6-M Architecture with SAIL

• Typ der Arbeit: Bachelorarbeit
• Status der Arbeit: reserviert
• Projekte: AHA
• Betreuer: Tim-Marek Thomas, Daniel Lohmann

Context🔗

In the CLASSY-FI project we derive constructive methods and techniques for scalable, yet precise and complete FI to experimentally assess the robustness of safety-critical embedded control systems against soft errors A new topic is the consideration of fault injection campaigns in a special setting: as continous integration tests. We try to provide answers for the following questions:

• How can we accelerate fault injection campaigns in the CI context?
• Can we do do this and still ensure accurate (enough) results?
• Are we able to fully verify a component and reuse the FI campaign results for other pieces of software, which include the component?

Problem🔗

We need more complex test applications than simple benchmarks suites such as MiBench¹ for the evaluation of our approaches. Especially important is a commit history, which is not provided using standard benchmark suites. Unfortunately, there are not many open-source applications, which target a savety critical domain. However, there are, e.g. flight frameworks for satellites (e.g. ⁶), and applications like LibrePilot². Applications like these typically target small ARM boards with CPUs from the Cortex-M series.

FAIL*³, the FI framework used in our project, currently supports two Arm emulation backends: gem5 (Armv8.0-A) and emulators based on SAIL⁴ models (Armv[8.5,9.3,9.4]-A). SAIL is a imperative language for describing the instruction-set architecture (ISA) semantics of processors. Given a SAIL definition, the tool can generate executable emulators in the C language. So, one can use definitions of different ISAs on the basis of one single tool including type and sanity checking.

Neither gem5 nor SAIL do cover the Armv[X]-M ISA.

Goal🔗

The main goal of this thesis is to implement a SAIL model (and thus ISA definition) for Armv6-M⁵, and integrate the generated emulator into FAIL*. A generic interface for this was already introduced in previous works (see related theses and the paper below).

More precisely, you are expected to take following steps:

• Literature search: Arm SAIL models, (more) potential tests applications
• Implement the Armv6-M model
• Verify it against a real hardware implementation
  • E.g. run several benchmarks from the MiBench benchmark suite and ensure after each step the same state
• Integrate the generated emulator into FAIL*
• Run a fault injection campaign for each of the verification benchmarks
  • Or optionally run the campaign for the fsfw⁶ or the librepilot²
• Optionally also implement a Armv7-M model

Topics: Arm ISA, Sail, (C/C++,cmake)

References🔗

SAFECOMP Conference B
SailFAIL: Model-Derived Simulation-Assisted ISA-Level Fault-Injection Platforms

Christian Dietrich, Malte Bargholz, Yannick Loeck, Marcel Budoj, Luca Nedaskowskij, Daniel Lohmann41st International Conference on Computer Safety, Reliability and Security (SAFECOMP 2022)Springer-Verlag2022.
PDF Slides 10.1007/978-3-031-14835-4_14 [BibTex]

×

BibTex Entry

@inproceedings{dietrich:22:safecomp,
location = {Munich, Germany},
author = {Dietrich, Christian and Bargholz, Malte and Loeck, Yannick and Budoj, Marcel and Nedaskowskij, Luca and Lohmann, Daniel},
booktitle = {41st International Conference on Computer Safety, Reliability and Security (SAFECOMP 2022)},
doi = {10.1007/978-3-031-14835-4_14},
entrysubtype = {Conference},
publisher = {Springer-Verlag},
title = {SailFAIL: Model-Derived Simulation-Assisted ISA-Level Fault-Injection Platforms},
year = {2022},
}

Close

Transient-Fault Resilience of a Capability-enabled Processor Plattform

Integration of SAIL-based MIPS and CHERI emulators into the FAIL* fault-injection tool and quantitative fault-resilience comparision. [PDF]

---

 

Typ

Masterarbeit

---

 

Status

abgeschlossen

---

 

Supervisors

Christian Dietrich
Daniel Lohmann

---

 

Project

CLASSY-FI

---

 

Bearbeiter

Malte Bargholz (abgegeben: 01. Nov 2020)

Formalizing the Execution Semantics of the AVR Instruction Set with the Description Language SAIL

Implementing the AVR-processor instruction-set architecture in SAIL for generating emulators automatically.

---

 

Typ

Bachelorarbeit

---

 

Status

abgeschlossen

---

 

Supervisors

Christian Dietrich
Oskar Pusz
Daniel Lohmann

---

 

Project

CLASSY-FI

---

 

Bearbeiter

Luca Nedaskovskij (abgegeben: 16. Oct 2020)

Schotbruch: Automatisierte Ableitung von Injektionsplattformen für transiente Hardwarefehler aus formalen Prozessormodellen

Use SAIL language to integrate an ISA implementations into a fault injection framework. Different CPU architectures shall be evaluated for reliability. [PDF]

---

 

Typ

Masterarbeit

---

 

Status

abgeschlossen

---

 

Supervisors

Christian Dietrich
Daniel Lohmann

---

 

Project

CLASSY-FI

---

 

Bearbeiter

Marcel Budoj (abgegeben: 08. May 2019)