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

• From Scientific Texts to Verifiable Code: Automating the Process with Transformers [2.536225150399618]
  transformers can read research papers that propose algorithms with formal proofs and translate these proofs into verifiable code. We argue that this approach can significantly reduce the barrier to formal verification.
  arXiv  Detail & Related papers  (2025-01-09T14:03:35Z)
• CryptoFormalEval: Integrating LLMs and Formal Verification for Automated Cryptographic Protocol Vulnerability Detection [41.94295877935867]
  We introduce a benchmark to assess the ability of Large Language Models to autonomously identify vulnerabilities in new cryptographic protocols. We created a dataset of novel, flawed, communication protocols and designed a method to automatically verify the vulnerabilities found by the AI agents.
  arXiv  Detail & Related papers  (2024-11-20T14:16:55Z)
• Improving LLM Reasoning through Scaling Inference Computation with Collaborative Verification [52.095460362197336]
  Large language models (LLMs) struggle with consistent and accurate reasoning. LLMs are trained primarily on correct solutions, reducing their ability to detect and learn from errors. We propose a novel collaborative method integrating Chain-of-Thought (CoT) and Program-of-Thought (PoT) solutions for verification.
  arXiv  Detail & Related papers  (2024-10-05T05:21:48Z)
• 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)
• 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)
• 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 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.