arXiv ScienceSearch

arXiv subjects

Piergiuseppe Mallozzi

Publications and source records attributed to Piergiuseppe Mallozzi.

5 recordsLinked to original sources

Deploying ZKP Frameworks with Real-World Data: Challenges and Proposed Solutions

Zero-knowledge proof (ZKP) frameworks have the potential to revolutionize the handling of sensitive data in various domains. However, deploying ZKP frameworks with real-world data presents several challenges, including scalability, usability, and interoperability. In this project, we present Fact Fortress, an end-to-end framework for designing and deploying zero-knowledge proofs of general statements. Our solution leverages proofs of data provenance and auditable data access policies to ensure the trustworthiness of how sensitive data is handled and provide assurance of the computations that have been performed on it. ZKP is mostly associated with blockchain technology, where it enhances transaction privacy and scalability through rollups, addressing the data inherent to the blockchain. Our approach focuses on safeguarding the privacy of data external to the blockchain, with the blockchain serving as publicly auditable infrastructure to verify the validity of ZK proofs and track how data access has been granted without revealing the data itself. Additionally, our framework provides high-level abstractions that enable developers to express complex computations without worrying about the underlying arithmetic circuits and facilitates the deployment of on-chain verifiers. Although our approach demonstrated fair scalability for large datasets, there is still room for improvement, and further work is needed to enhance its scalability. By enabling on-chain verification of computation and data provenance without revealing any information about the data itself, our solution ensures the integrity of the computations on the data while preserving its privacy.

cs.CR

Correct-by-Construction Design of Contextual Robotic Missions Using Contracts

Effectively specifying and implementing robotic missions poses a set of challenges to software engineering for robotic systems. These challenges stem from the need to formalize and execute a robot's high-level tasks while considering various application scenarios and conditions, also known as contexts, in real-world operational environments. Writing correct mission specifications that explicitly account for multiple contexts can be tedious and error-prone. Furthermore, as the number of contexts, and consequently the complexity of the specification, increases, generating a correct-by-construction implementation (e.g., by using synthesis methods) can become intractable. A viable approach to address these issues is to decompose the mission specification into smaller, manageable sub-missions, with each sub-mission tailored to a specific context. Nevertheless, this compositional approach introduces its own set of challenges in ensuring the overall mission's correctness. In this paper, we propose a novel compositional framework for specifying and implementing contextual robotic missions using assume-guarantee contracts. The mission specification is structured in a hierarchical and modular fashion, allowing for each sub-mission to be synthesized as an independent robot controller. We address the problem of dynamically switching between sub-mission controllers while ensuring correctness under predefined conditions.

cs.SE

Pacti: Scaling Assume-Guarantee Reasoning for System Analysis and Design

Contract-based design is a method to facilitate modular system design. While there has been substantial progress on the theory of contracts, there has been less progress on scalable algorithms for the algebraic operations in this theory. In this paper, we present: 1) principles to implement a contract-based design tool at scale and 2) Pacti, a tool that can efficiently compute these operations. We then illustrate the use of Pacti in a variety of case studies.

cs.LO

A Grammar for the Representation of Unmanned Aerial Vehicles with 3D Topologies

We propose a context-sensitive grammar for the systematic exploration of the design space of the topology of 3D robots, particularly unmanned aerial vehicles. It defines production rules for adding components to an incomplete design topology modeled over a 3D grid. The rules are local. The grammar is simple, yet capable of modeling most existing UAVs as well as novel ones. It can be easily generalized to other robotic platforms. It can be thought of as a building block for any design exploration and optimization algorithm.

cs.RO

Contract-Based Specification Refinement and Repair for Mission Planning

We address the problem of modeling, refining, and repairing formal specifications for robotic missions using assume-guarantee contracts. We show how to model mission specifications at various levels of abstraction and implement them using a library of pre-implemented specifications. Suppose the specification cannot be met using components from the library. In that case, we compute a proxy for the best approximation to the specification that can be generated using elements from the library. Afterward, we propose a systematic way to either 1) search for and refine the `missing part' of the specification that the library cannot meet or 2) repair the current specification such that the existing library can refine it. Our methodology for searching and repairing mission requirements leverages the quotient, separation, composition, and merging operations between contracts.

cs.RO