Trustworthy Distributed Certification of Program Execution
- URL: http://arxiv.org/abs/2402.13792v1
- Date: Wed, 21 Feb 2024 13:21:37 GMT
- Title: Trustworthy Distributed Certification of Program Execution
- Authors: Alex Wolf, Marco Eduardo Palma, Pasquale Salza, Harald C. Gall
- Abstract summary: We propose an innovative approach that combines a prototype programming language called Mona with a certification protocol OCCP.
Our protocol allows for certification of program segments in a distributed, immutable, and trustworthy system without the need for naive re-execution.
Our findings demonstrate the efficiency of our approach in reducing the number of program executions compared to existing state-of-the-art methods.
- Score: 2.208443815105053
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: Verifying the execution of a program is complicated and often limited by the
inability to validate the code's correctness. It is a crucial aspect of
scientific research, where it is needed to ensure the reproducibility and
validity of experimental results. Similarly, in customer software testing, it
is difficult for customers to verify that their specific program version was
tested or executed at all. Existing state-of-the-art solutions, such as
hardware-based approaches, constraint solvers, and verifiable computation
systems, do not provide definitive proof of execution, which hinders reliable
testing and analysis of program results. In this paper, we propose an
innovative approach that combines a prototype programming language called Mona
with a certification protocol OCCP to enable the distributed and decentralized
re-execution of program segments. Our protocol allows for certification of
program segments in a distributed, immutable, and trustworthy system without
the need for naive re-execution, resulting in significant improvements in terms
of time and computational resources used. We also explore the use of blockchain
technology to manage the protocol workflow following other approaches in this
space. Our approach offers a promising solution to the challenges of program
execution verification and opens up opportunities for further research and
development in this area. Our findings demonstrate the efficiency of our
approach in reducing the number of program executions compared to existing
state-of-the-art methods, thus improving the efficiency of certifying program
executions.
Related papers
- AGORA: Open More and Trust Less in Binary Verification Service [16.429846973928512]
We introduce a novel binary verification service, AGORA, scrupulously designed to overcome the challenge.
Certain tasks can be delegated to untrusted entities, while the corresponding validators are securely housed within the trusted computing base.
Through a novel blockchain-based bounty task manager, it also utilizes crowdsourcing to remove trust in theorem provers.
arXiv Detail & Related papers (2024-07-21T05:29:22Z) - HUWSOD: Holistic Self-training for Unified Weakly Supervised Object Detection [66.42229859018775]
We introduce a unified, high-capacity weakly supervised object detection (WSOD) network called HUWSOD.
HUWSOD incorporates a self-supervised proposal generator and an autoencoder proposal generator with a multi-rate re-supervised pyramid to replace traditional object proposals.
Our findings indicate that randomly boxes, although significantly different from well-designed offline object proposals, are effective for WSOD training.
arXiv Detail & Related papers (2024-06-27T17:59:49Z) - Formally Verified Approximate Policy Iteration [11.602089225841633]
We show how the formalized algorithm can be refined to an executable, verified implementation.
The implementation is evaluated on benchmark problems to show its practicability.
As part of the refinement, we develop verified software to certify Linear Programming solutions.
arXiv Detail & Related papers (2024-06-11T15:07:08Z) - Finding Software Vulnerabilities in Open-Source C Projects via Bounded
Model Checking [2.9129603096077332]
We advocate that bounded model-checking techniques can efficiently detect vulnerabilities in general software systems.
We have developed and evaluated a methodology to verify large software systems using a state-of-the-art bounded model checker.
arXiv Detail & Related papers (2023-11-09T11:25:24Z) - Using Machine Learning To Identify Software Weaknesses From Software
Requirement Specifications [49.1574468325115]
This research focuses on finding an efficient machine learning algorithm to identify software weaknesses from requirement specifications.
Keywords extracted using latent semantic analysis help map the CWE categories to PROMISE_exp. Naive Bayes, support vector machine (SVM), decision trees, neural network, and convolutional neural network (CNN) algorithms were tested.
arXiv Detail & Related papers (2023-08-10T13:19:10Z) - Benchopt: Reproducible, efficient and collaborative optimization
benchmarks [67.29240500171532]
Benchopt is a framework to automate, reproduce and publish optimization benchmarks in machine learning.
Benchopt simplifies benchmarking for the community by providing an off-the-shelf tool for running, sharing and extending experiments.
arXiv Detail & Related papers (2022-06-27T16:19:24Z) - Learning from Self-Sampled Correct and Partially-Correct Programs [96.66452896657991]
We propose to let the model perform sampling during training and learn from both self-sampled fully-correct programs and partially-correct programs.
We show that our use of self-sampled correct and partially-correct programs can benefit learning and help guide the sampling process.
Our proposed method improves the pass@k performance by 3.1% to 12.3% compared to learning from a single reference program with MLE.
arXiv Detail & Related papers (2022-05-28T03:31:07Z) - Part-X: A Family of Stochastic Algorithms for Search-Based Test
Generation with Probabilistic Guarantees [3.9119084077397863]
falsification has proven to be a practical and effective method for discovering erroneous behaviors in Cyber-Physical Systems.
Despite the constant improvements on the performance and applicability of falsification methods, they all share a common characteristic.
They are best-effort methods which do not provide any guarantees on the absence of erroneous behaviors (falsifiers) when the testing budget is exhausted.
arXiv Detail & Related papers (2021-10-20T19:05:00Z) - Test case prioritization using test case diversification and
fault-proneness estimations [0.0]
We propose an approach for TCP that takes into account test case coverage data, bug history, and test case diversification.
The diversification of test cases is preserved by incorporating fault-proneness on a clustering-based approach scheme.
The experiments show that the proposed methods are superior to coverage-based TCP methods.
arXiv Detail & Related papers (2021-06-19T15:55:24Z) - Learning from Executions for Semantic Parsing [86.94309120789396]
We focus on the task of semi-supervised learning where a limited amount of annotated data is available.
We propose to encourage executable programs for unlabeled utterances.
arXiv Detail & Related papers (2021-04-12T21:07:53Z) - Global Optimization of Objective Functions Represented by ReLU Networks [77.55969359556032]
Neural networks can learn complex, non- adversarial functions, and it is challenging to guarantee their correct behavior in safety-critical contexts.
Many approaches exist to find failures in networks (e.g., adversarial examples), but these cannot guarantee the absence of failures.
We propose an approach that integrates the optimization process into the verification procedure, achieving better performance than the naive approach.
arXiv Detail & Related papers (2020-10-07T08:19:48Z)
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.