Towards Formal Verification of a TPM Software Stack
- URL: http://arxiv.org/abs/2307.16821v2
- Date: Fri, 27 Oct 2023 15:29:06 GMT
- Title: Towards Formal Verification of a TPM Software Stack
- Authors: Yani Ziani and Nikolai Kosmatov and Fr\'ed\'eric Loulergue and Daniel
Gracia P\'erez and T\'eo Bernier
- Abstract summary: This paper describes a case study on formal verification of tpm2-tss using the Frama-C verification platform.
Heavily based on linked lists and complex data structures, the library code appears to be highly challenging for the verification tool.
- Score: 0.5074812070492739
- License: http://creativecommons.org/licenses/by-nc-nd/4.0/
- Abstract: The Trusted Platform Module (TPM) is a cryptoprocessor designed to protect
integrity and security of modern computers. Communications with the TPM go
through the TPM Software Stack (TSS), a popular implementation of which is the
open-source library tpm2-tss. Vulnerabilities in its code could allow attackers
to recover sensitive information and take control of the system. This paper
describes a case study on formal verification of tpm2-tss using the Frama-C
verification platform. Heavily based on linked lists and complex data
structures, the library code appears to be highly challenging for the
verification tool. We present several issues and limitations we faced,
illustrate them with examples and present solutions that allowed us to verify
functional properties and the absence of runtime errors for a representative
subset of functions. We describe verification results and desired tool
improvements necessary to achieve a full formal verification of the target
code.
Related papers
- DetToolChain: A New Prompting Paradigm to Unleash Detection Ability of MLLM [81.75988648572347]
We present DetToolChain, a novel prompting paradigm to unleash the zero-shot object detection ability of multimodal large language models (MLLMs)
Our approach consists of a detection prompting toolkit inspired by high-precision detection priors and a new Chain-of-Thought to implement these prompts.
We show that GPT-4V with our DetToolChain improves state-of-the-art object detectors by +21.5% AP50 on MS Novel class set for open-vocabulary detection.
arXiv Detail & Related papers (2024-03-19T06:54:33Z) - DT-SIM: Property-Based Testing for MPC Security [2.0308771704846245]
Property-based testing is effective for detecting security bugs in secure protocols.
We specifically target Secure Multi-Party Computation (MPC)
We devise a test that can detect various flaws in a bit-level implementation of an MPC protocol.
arXiv Detail & Related papers (2024-03-08T02:02:24Z) - HasTEE+ : Confidential Cloud Computing and Analytics with Haskell [50.994023665559496]
Confidential computing enables the protection of confidential code and data in a co-tenanted cloud deployment using specialized hardware isolation units called Trusted Execution Environments (TEEs)
TEEs offer low-level C/C++-based toolchains that are susceptible to inherent memory safety vulnerabilities and lack language constructs to monitor explicit and implicit information-flow leaks.
We address the above with HasTEE+, a domain-specific language (cla) embedded in Haskell that enables programming TEEs in a high-level language with strong type-safety.
arXiv Detail & Related papers (2024-01-17T00:56:23Z) - QR TPM in Programmable Low-Power Devices [2.8007688938043622]
We investigate the deployment of Quantum Resistant (QR) primitives and protocols in the standard TPM 2.0.
In particular, the Kyber algorithm for key encapsulation, the Dilithium algorithm for digital signature, and a 3-round Random Oblivious Transfer (ROT) protocol.
This paper also shows that it would be possible to backport the required code to ensure that current TPMs remain secure against quantum adversaries.
arXiv Detail & Related papers (2023-09-29T17:21:46Z) - Rely-guarantee Reasoning about Concurrent Memory Management:
Correctness, Safety and Security [0.0]
An incorrect specification and implementation of the memory management may lead to system crashes or exploitable attacks.
This article presents the first formal specification and mechanized proof of a concurrent memory management for a real-world OS.
arXiv Detail & Related papers (2023-09-17T03:41:10Z) - A General Verification Framework for Dynamical and Control Models via Certificate Synthesis [54.959571890098786]
We provide a framework to encode system specifications and define corresponding certificates.
We present an automated approach to formally synthesise controllers and certificates.
Our approach contributes to the broad field of safe learning for control, exploiting the flexibility of neural networks.
arXiv Detail & Related papers (2023-09-12T09:37:26Z) - A Novel Approach to Identify Security Controls in Source Code [4.598579706242066]
This paper enumerates a comprehensive list of commonly used security controls and creates a dataset for each one of them.
It uses the state-of-the-art NLP technique Bidirectional Representations from Transformers (BERT) and the Tactic Detector from our prior work to show that security controls could be identified with high confidence.
arXiv Detail & Related papers (2023-07-10T21:14:39Z) - (Security) Assertions by Large Language Models [25.270188328436618]
We investigate the use of emerging large language models (LLMs) for code generation in hardware assertion generation for security.
We focus our attention on a popular LLM and characterize its ability to write assertions out of the box, given varying levels of detail in the prompt.
arXiv Detail & Related papers (2023-06-24T17:44:36Z) - Monitoring ROS2: from Requirements to Autonomous Robots [58.720142291102135]
This paper provides an overview of a formal approach to generating runtime monitors for autonomous robots from requirements written in a structured natural language.
Our approach integrates the Formal Requirement Elicitation Tool (FRET) with Copilot, a runtime verification framework, through the Ogma integration tool.
arXiv Detail & Related papers (2022-09-28T12:19:13Z) - Towards Semantic Communication Protocols: A Probabilistic Logic
Perspective [69.68769942563812]
We propose a semantic protocol model (SPM) constructed by transforming an NPM into an interpretable symbolic graph written in the probabilistic logic programming language (ProbLog)
By leveraging its interpretability and memory-efficiency, we demonstrate several applications such as SPM reconfiguration for collision-avoidance.
arXiv Detail & Related papers (2022-07-08T14:19:36Z) - Conformance Checking with Uncertainty via SMT (Extended Version) [66.58864135810981]
We show how to solve the problem of checking conformance of uncertain logs against data-aware reference processes.
Our approach is modular, in that it homogeneously accommodates for different types of uncertainty.
We show the correctness of our approach and witness feasibility through a proof-of-concept implementation.
arXiv Detail & Related papers (2022-06-15T11:39:45Z)
This list is automatically generated from the titles and abstracts of the papers in this site.
This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.