Clash Formal
Clash Formal will die Anwendbarkeit formaler Verifikationswerkzeuge wie Beweisassistenten oder SMT-Löser nicht nur für funktionale Programme, sondern in gleicher Weise auch für intrinsisch parallele funktionale Schaltungsdesigns ermöglichen.
Ziel des Projekts ist es, die Leistungsfähigkeit funktionaler Sprachen für die präzise Beschreibung von Hardware- und Softwarefunktionalität in Kombination mit einem starken Typsystem zu nutzen, um das gesamte Spektrum nicht-funktionaler Sicherheitsanforderungen abzudecken.
Zu diesem Zweck nutzen sie Clash, eine funktionale Hardwarebeschreibungssprache, deren Syntax und Semantik der funktionalen Programmiersprache Haskell entlehnt sind. Sie bietet einen vertrauten strukturellen Designansatz für kombinatorische und synchrone sequentielle Schaltungen. Der Clash-Compiler wandelt funktionale high-level Hardwarebeschreibungen in synthetisierbare low-level Sprachen, wie VHDL, Verilog oder SystemVerilog um.
Ihr besonderer Schwerpunkt liegt auf der formalen Verifikation funktionaler Hardware-Designs gemeinsam mit denHardware-Software-Schnittstellen. Ihr Ziel ist es, ein voll ausgestattetes Ökosystem aus eng miteinander verbundenen Designtools und Methodiken zu schaffen, das das gesamte Spektrum von Software, Hardware und formalem Beweisen sowie die damit verbundenen Methodiken abdeckt.
Das Clash-Ökosystem bietet eine perfekte Verbindung zwischen Hardware- und Programmdesign durch die Verwendung des gemeinsamen Haskell-Sprach-Frontends. Gleichzeitig lässt es sich aufgrund der zugrunde liegenden funktionalen Designprinzipien gut mit formalen Verifikationswerkzeugen wie Beweisassistenten oder Modellprüfern verbinden. In diesem Projekt bauen wir auf diesen Verbindungen auf, um sie auf jeder Ebene eines IT-Hardware-Software-Stacks anwendbar und zugänglich zu machen.
Clash Formal wird von QBayLogic BV betrieben.
Ziele von Clash Formal
- Entwicklung eines formal verifizierten Krypto-Kerns in Clash, der sichere Hash-Funktionen und elliptische Kurvenkryptografie unterstützt, wobei alle verwendeten Primitive nachweislich gegen bekannte Side-Channel-Angriffe resistent sind.
- Entwicklung eines verifizierten Hardware-Stacks, der Passkey-Funktionalität über FIDO2 und CTAP2 über USB unterstützt.
- Integration einer formal verifizierten RISC-V-CPU auf Basis von Sail mit CHERI-Unterstützung.
- Erweiterung und Einbindung von automatisierten und maschinell überprüfbaren Beweisen in die funktionalen Sprachen Haskell und Clash, sodass diese eng mit dem bereits vorhandenen starken Typsystem der Sprache integriert sind.
- Eine einzige Sprachlösung für die Spezifikation, Formalisierung und Verifikation von miteinander verbundenen Hardware- und Softwareeigenschaften.
Clash Formal hat sich folgende Ziele gesetzt:
- Entwicklung eines formal verifizierten Krypto-Kerns in Clash, der sichere Hash-Funktionen und elliptische Kurvenkryptografie unterstützt, wobei alle verwendeten Primitiven nachweislich gegen bekannte Side-Channel-Angriffe resistent sind.
- Entwicklung eines verifizierten Hardware-Stacks, der Passkey-Funktionalität über FIDO2 und CTAP2 über USB unterstützt.
- Integration einer formal verifizierten RISC-V-CPU auf Basis von Sail mit CHERI-Unterstützung.
- Erweiterung und Einbindung von maschinell überprüfbaren Beweisen sowie automatisierten Schlussfolgerungslösungen in die funktionalen Sprachen Haskell und Clash, sodass diese eng mit dem bereits vorhandenen starken Typsystem der Sprache integriert sind.
- Eine einzige Sprachlösung für die Spezifikation, Formalisierung und Verifikation von miteinander verbundenen Hardware- und Softwareeigenschaften.
Betrag zur formalen Verifikation
Demonstrator
Clash Formal wird einen fortschrittlichen Smartcard-Systemdemonstrator bis zu TRL4 entwickeln, der einen verifizierten RISC-V-Prozessor, verifizierte Hardware-Kryptografie und einen verifizierten Software-Stack in einem einzigen System-on-Chip-Design integriert. Darüber hinaus wird das entwickelte System über eine Passkey-Funktionalität basierend auf dem FIDO2-Standard und dem Client-to-Authenticator Protocol (CTAP2) verfügen. Es wird auch ein minimal verifiziertes Smartcard-Betriebssystem integrieren, das nachweisbare Hardware-/Software-Verträge über eine einzige Sprache und ein konstruktionsgemäß korrektes Design nutzt.
