Verifying components of Arm(R) Confidential Computing Architecture with ESBMC

• URL: http://arxiv.org/abs/2406.04375v1
• Date: Wed, 5 Jun 2024 09:09:37 GMT
• Title: Verifying components of Arm(R) Confidential Computing Architecture with ESBMC
• Authors: Tong Wu, Shale Xiong, Edoardo Manino, Gareth Stockwell, Lucas C. Cordeiro,
• Abstract summary: Realm Management Monitor (RMM) is an essential firmware component within the recent Arm Confidential Computing Architecture (Arm CCA) Previous work applies formal verification techniques to verify the specification and prototype reference implementation of RMM. This paper discusses the application of ESBMC, a state-of-the-art Satisfiability Modulo Theories (SMT)-based software model checker, to further enhance RRM verification.
• Score: 6.914213030256384
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Realm Management Monitor (RMM) is an essential firmware component within the recent Arm Confidential Computing Architecture (Arm CCA). Previous work applies formal techniques to verify the specification and prototype reference implementation of RMM. However, relying solely on a single verification tool may lead to the oversight of certain bugs or vulnerabilities. This paper discusses the application of ESBMC, a state-of-the-art Satisfiability Modulo Theories (SMT)-based software model checker, to further enhance RRM verification. We demonstrate ESBMC's ability to precisely parse the source code and identify specification failures within a reasonable time frame. Moreover, we propose potential improvements for ESBMC to enhance its efficiency for industry engineers. This work contributes to exploring the capabilities of formal verification techniques in real-world scenarios and suggests avenues for further improvements to better meet industrial verification needs.

Related papers

• Towards commands recommender system in BIM authoring tool using transformers [0.7499722271664147]
  This study explores the potential of sequential recommendation systems to accelerate the BIM modeling process. By treating BIM software commands as recommendable items, we introduce a novel end-to-end approach that predicts the next-best command based on user historical interactions.
  arXiv  Detail & Related papers  (2024-06-02T17:47:06Z)
• A Provably Effective Method for Pruning Experts in Fine-tuned Sparse Mixture-of-Experts [49.394145046409044]
  This paper provides the first provably efficient technique for pruning experts in finetuned MoE models. We theoretically prove that prioritizing the pruning of the experts with a smaller change of the routers l2 norm from the pretrained model guarantees the preservation of test accuracy. Although our theoretical analysis is centered on binary classification tasks on simplified MoE architecture, our expert pruning method is verified on large vision MoE models.
  arXiv  Detail & Related papers  (2024-05-26T17:52:58Z)
• Skills Composition Framework for Reconfigurable Cyber-Physical Production Modules [44.99833362998488]
  This paper proposes a framework for skills' composition and execution in skill-based reconfigurable cyber-physical production modules. It is based on distributed Behavior trees (BTs) and provides good integration between low-level devices' specific code and AI-based task-oriented frameworks.
  arXiv  Detail & Related papers  (2024-05-22T12:56:05Z)
• OSM: Leveraging Model Checking for Observing Dynamic 1 behaviors in Aspect-Oriented Applications [0.0]
  observe-based statistical model-checking (OSM) framework devised to craft executable formal models directly from foundational system code. This ensures the unyielding performance of electronic health record systems amidst shifting preconditions.
  arXiv  Detail & Related papers  (2024-03-03T00:03:34Z)
• ESBMC v7.4: Harnessing the Power of Intervals [4.6232063855710654]
  ESBMC implements many state-of-the-art techniques for model checking. New features allow us to obtain verification results for unsupported programs and properties. ESBMC employs a new interval analysis of expressions in programs to increase verification performance.
  arXiv  Detail & Related papers  (2023-12-22T14:56:46Z)
• A General Framework for Verification and Control of Dynamical 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 New Era in Software Security: Towards Self-Healing Software via Large Language Models and Formal Verification [8.733354577147093]
  This paper introduces an innovative approach that combines Large Language Models (LLMs) with Formal Verification strategies for automatic software vulnerability repair. We present the ESBMC-AI framework as a proof of concept, leveraging the well-recognized and industry-adopted Efficient SMT-based Context-Bounded Model Checker (ESBMC) and a pre-trained transformer model. Our results demonstrate ESBMC-AI's capability to automate the detection and repair of issues such as buffer overflow, arithmetic overflow, and pointer dereference failures with high accuracy.
  arXiv  Detail & Related papers  (2023-05-24T05:54:10Z)
• Relational Action Bases: Formalization, Effective Safety Verification, and Invariants (Extended Version) [67.99023219822564]
  We introduce the general framework of relational action bases (RABs) RABs generalize existing models by lifting both restrictions. We demonstrate the effectiveness of this approach on a benchmark of data-aware business processes.
  arXiv  Detail & Related papers  (2022-08-12T17:03:50Z)
• MMOCR: A Comprehensive Toolbox for Text Detection, Recognition and Understanding [70.16678926775475]
  MMOCR is an open-source toolbox for text detection and recognition. It implements 14 state-of-the-art algorithms, which is more than all the existing open-source OCR projects we are aware of to date.
  arXiv  Detail & Related papers  (2021-08-14T14:10:23Z)
• Explanations of Machine Learning predictions: a mandatory step for its application to Operational Processes [61.20223338508952]
  Credit Risk Modelling plays a paramount role. Recent machine and deep learning techniques have been applied to the task. We suggest to use LIME technique to tackle the explainability problem in this field.
  arXiv  Detail & Related papers  (2020-12-30T10:27:59Z)

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.