Skip to main content
To KTH's start page

Trustfull: Trustworthy Fullstack Computing

The Trustfull project, funded by Stiftelsen för Strategisk Forskning (SSF), aims to show that formal techniques can be used in combination with intelligent static and dynamic program manipulation techniques at scale to significantly strengthen the security of real life application stacks. The focus is on software-based attacks: attacks manifested through software that affect the host systems in adversarial ways through bugs, vulnerabilities, and design deficiencies at any level in the software stack.

The project brings together different research groups, the group of Dam and Guanciale with deep experience in provable security and low level execution platforms from the previous SSF-supported PROSPER project, and the groups of Baudry and Monperrus, with extensive experience in large scale software engineering, software diversity, and automated program repair.

The proposed research program involves three main components:
• Theories and tools for formal modelling, security analysis, and program manipulation at the level of processor architecture, firmware, kernel and application code.
• Defensive mechanisms that use formal methods and diversity-based techniques in innovative ways for application hardening at both application and system level.
• A core demonstrator application, an electronic voting system, serving as the main tool for focusing project work and evaluating the results.

This project is funded by SSF, see https://strategiska.se/pressmeddelande/300-miljoner-till-cybersakerhet-en-strategisk-injektion/

People

The team (alphabetical order):

News & Events

Media

Data

Software

  • Algorand Verification
  • Verified model of the Algorand consensus protocol in Coq
  • Coq
  • Proof assistant and formal language for executable algorithms and theorems
  • Chip
  • Verified change impact analysis Coq library and OCaml-based tool
  • DepClean
  • Tool for automatically removing unused dependencies from Java projects
  • Giskard verification
  • Verified model of the Giskard consensus protocol in Coq
  • Hydras & Co.
  • Collaborative, documented library of discrete mathematics for Coq
  • HolBA
  • Binary analysis library for the HOL4 proof assistant
  • HOL4P4
  • mCoq
  • Mutation analysis tool for Coq verification projects
  • MIL
  • Formalization and tools in the HOL4 theorem prover of a machine independent language for defining the semantics of microarchitectural features such as out-of-order execution.
  • OpenMZ
  • Security kernel for embedded RISC-V applications
  • Ott
  • Tool for writing definitions of programming languages and calculi that can be translated to Coq and HOL4
  • Repairnator
  • Software development bot that automatically repairs build failures on continuous integration
  • Roosterize
  • Tool for suggesting lemma names in Coq verification projects
  • Scam-V
  • Abstract side channel model validation framework
  • SequenceR
  • seq2seq system to do bug fixes in source code change at the line level
  • SerAPI
  • Library and tools for (de)serialization of Coq code to and from JSON and S-expressions
  • Slumps
  • Research project on superoptimization, diversification (CROW) for WebAssembly WASM
  • Sorald
  • An automatic repair system for bug and vulnerability warnings in Java
  • Spoon
  • Metaprogramming library to analyze and transform Java source code, supporting Java 9, 10, and 11
  • Tarjan and Kosaraju
  • Verified implementation in Coq of topological sorting with extended guarantees for acyclic graphs
  • Templates for Coq projects
  • Template files for use in generating configuration files for Coq
  • VLSM
  • Formalized model in Coq for stating and solving distributed consensus problems
  • VRepair
  • AI system for for repairing vulnerabilities in C
  • Wasm-mutate
  • a new tool for fuzzing Wasm compilers, runtimes, validators, and other Wasm-consuming programs
  • xPerturb
  • Perturbation analysis, correctness attraction and randomization

Talks

  • EclipseCon 2022
  • Let a bot deal with your static analysis warnings backlog
  • Speaker: Aman Sharma
  • FMCAD 2021
  • Refinement-Based Verification of Device-to-Device Information Flow (Video)
  • Speaker: Ning Dong
  • Coq Users and Developers Workshop 2020
  • Towards better Coq batch incremental proving (Video)
  • Demonstration of Roosterize, a tool for suggesting Coq lemma names using deep learning (Video)
  • Speaker: Karl Palmskog
  • CCS 2020
  • InSpectre: Breaking and Fixing Microarchitectural Vulnerabilities by Formal Analysis (Video)
  • Speaker: Roberto Guanciale
  • CAV 2020
  • Scam-V: validation of abstract side channel models for computer architectures (Video)
  • Speaker: Andreas Lindner
  • ICSE 2020
  • SequenceR: sequence-to-sequence learning for end-to-end program repair (Video)
  • Speaker: Steve Kommrusch
  • MoreVMs’20
  • Superoptimization of WebAsssembly Bytecode (Video)
  • Speaker: Javier Cabrera

Publications