Searcharxiv⌕ Search

arXiv subjects

César Sánchez

Publications and source records attributed to César Sánchez.

At least 19 recordsLinked to original sources

The optical architecture of a heterogenous quantum network deployed in production facilities

Quantum Communications promise advances in cryptography, quantum computing and clock synchronisation, among other emerging applications. However, communication based on quantum phenomena requires an extreme level of isolation from external disturbances, complicating the co-propagation of quantum and classical signals. The challenge is greater when deploying networks that are both heterogeneous (e.g., multiple vendors) and installed in production facilities, given that this type of infrastructure already supports networks loaded with their own requirements. Moreover, to achieve a broad acceptance among network operators, the joint management and operation of quantum and classical resources, compliance with standards, and legal and quality assurance need to be addressed. This article presents solutions to the aforementioned challenges validated in the Madrid quantum network during the implementation of the projects CiViC and OpenQKD. This network was designed to integrate quantum communications in the telecommunications ecosystem by installing quantum-key-distribution modules from multiple providers in production nodes of two different operators. The modules were connected through an optically-switched network with more than 130~km of deployed optical fibre. The tests were done in compliance with strict service level agreements that protected the legacy traffic of the pre-existing classical network. The goal was to ensure full quantum-classical interoperability at all levels, while limiting the modifications to optical transport and encryption and complying with relevant standards. This effort is intended to lay the foundation for large-scale quantum network deployments.

quant-ph↗

HyperQB: A Bounded Model Checker for Hyperproperties

We introduce the tool HyperQB 2.0, the first highly efficient push-button bounded model checker (BMC) for hyperproperties. HyperQB takes as input a model in NuSMV or Verilog and a formula expressed in the temporal logics HyperLTL or A-HLTL. The core decision procedures to implement BMC are SMT and QBF solvers, enabling verification of finite- and infinite-state programs. HyperQB offers command-line and standalone graphical, and web-based interfaces. Based on the selection of either bug-hunting or synthesis, instances of counterexamples or path witnesses are returned. The tool is entirely implemented in Rust and we report on successful and effective model checking results for a rich set of experiments on a variety of case studies with rigorous performance comparison and contrast with similar tools.

cs.LO↗

Setchain Algorithms for Blockchain Scalability

Setchain has been proposed to increase blockchain scalability by relaxing the strict total order requirement among transactions. Setchain organizes elements into a sequence of sets, referred to as epochs, so that elements within each epoch are unordered. In this paper, we propose and evaluate three distinct Setchain algorithms, that leverage an underlying block-based ledger. Vanilla is a basic implementation that serves as a reference point. Compresschain aggregates elements into batches, and compresses these batches before appending them as epochs in the ledger. Hashchain converts batches into fixed-length hashes which are appended as epochs in the ledger. This requires Hashchain to use a distributed service to obtain the batch contents from its hash. To allow light clients to safely interact with only one server, the proposed algorithms maintain, as part of the Setchain, proofs for the epochs. An epoch-proof is the hash of the epoch, cryptographically signed by a server. A client can verify the correctness of an epoch with $f+1$ epoch-proofs (where $f$ is the maximum number of Byzantine servers assumed). All three Setchain algorithms are implemented on top of the CometBFT blockchain application platform. We conducted performance evaluations across various configurations, using clusters of four, seven, and ten servers. Our results show that the Setchain algorithms reach orders of magnitude higher throughput than the underlying blockchain, and achieve finality with latency below 4 seconds.

cs.DC↗

A Secure Sequencer and Data Availability Committee for Rollups (Extended Version)

Blockchains face a scalability limitation, partly due to the throughput limitations of consensus protocols, especially when aiming to obtain a high degree of decentralization. Layer 2 Rollups (L2s) are a faster alternative to conventional blockchains. L2s perform most computations offchain using minimally blockchains (L1) under-the-hood to guarantee correctness. A sequencer is a service that receives offchain L2 transaction requests, batches these transactions, and commits compressed or hashed batches to L1. Using hashing needs less L1 space, which is beneficial for gas cost, but requires a data availability committee (DAC) service to translate hashes into their corresponding batches of transaction requests. The behavior of sequencers and DACs influence the evolution of the L2 blockchain, presenting a potential security threat and delaying L2 adoption. We propose in this paper fraud-proof mechanisms, arbitrated by L1 contracts, to detect and generate evidence of dishonest behavior of the sequencer and DAC. We study how these fraud-proofs limit the power of adversaries that control different number of sequencer and DACs members, and provide incentives for their honest behavior. We designed these fraud-proof mechanisms as two player games. Unlike the generic fraud-proofs in current L2s (designed to guarantee the correct execution of transactions), our fraud-proofs are over pred-etermined algorithms that verify the properties that determine the correctness of the DAC. Arbitrating over concrete algorithms makes our fraud-proofs more efficient, easier to understand, and simpler to prove correct. We provide as an artifact a mechanization in LEAN4 of our fraud-proof games, including (1) the verified strategies that honest players should play to win all games as well as (2) mechanisms to detect dishonest claims.

cs.CR↗

A Decentralized Sequencer and Data Availability Committee for Rollups Using Set Consensus

Blockchains face a scalability challenge due to the intrinsic throughput limitations of consensus protocols and the limitation in block sizes due to decentralization. An alternative to improve the number of transactions per second is to use Layer 2 (L2) rollups. L2s perform most computations offchain using blockchains (L1) minimally under-the-hood to guarantee correctness. A sequencer receives offchain L2 transaction requests, batches them, and commits compressed or hashed batches to L1. Hashing offers much better compression but requires a data availability committee (DAC) to translate hashes back into their corresponding batches. Current L2s consist of a centralized sequencer which receives and serializes all transactions and an optional DAC. Centralized sequencers can undesirably influence L2s evolution. We propose in this paper a fully decentralized implementation of a service that combines (1) a sequencer that posts hashes to the L1 blockchain and (2) the data availability committee that reverses the hashes. We call the resulting service a (decentralized) arranger. Our decentralized arranger is based on Set Byzantine Consensus (SBC), a service where participants can propose sets of values and consensus is reached on a subset of the union of the values proposed. We extend SBC for our fully decentralized arranger. Our main contributions are (1) a formal definition of arrangers; (2) two implementations, one with a centralized sequencer and another with a fully decentralized algorithm, with their proof of correctness; and (3) empirical evidence that our solution scales by implementing all building blocks necessary to implement a correct server.

cs.DC↗

Temporal Hyperproperties for Population Protocols

Hyperproperties are properties over sets of traces (or runs) of a system, as opposed to properties of just one trace. They were introduced in 2010 and have been much studied since, in particular via an extension of the temporal logic LTL called HyperLTL. Most verification efforts for HyperLTL are restricted to finite-state systems, usually defined as Kripke structures. In this paper we study hyperproperties for an important class of infinite-state systems. We consider population protocols, a popular distributed computing model in which arbitrarily many identical finite-state agents interact in pairs. Population protocols are a good candidate for studying hyperproperties because the main decidable verification problem, well-specification, is a hyperproperty. We first show that even for simple (monadic) formulas, HyperLTL verification for population protocols is undecidable. We then turn our attention to immediate observation population protocols, a simpler and well-studied subclass of population protocols. We show that verification of monadic HyperLTL formulas without the next operator is decidable in 2-EXPSPACE, but that all extensions make the problem undecidable.

cs.LO↗

Unifying Asynchronous Logics for Hyperproperties

We introduce and investigate a powerful hyper logical framework in the linear-time setting, we call generalized HyperLTL with stuttering and contexts (GHyperLTL_SC for short). GHyperLTL_SC unifies known asynchronous extensions of HyperLTL and the well-known extension KLTL of LTL with knowledge modalities under both the synchronous and asynchronous perfect recall semantics. As a main contribution, we individuate a meaningful fragment of GHyperLTL_SC, we call simple GHyperLTL_SC, with a decidable model-checking problem, which is more expressive than HyperLTL and known fragments of asynchronous extensions of HyperLTL with a decidable model-checking problem. Simple GHyperLTL_SC subsumes KLTL under the synchronous semantics and the one-agent fragment of KLTL under the asynchronous semantics, and to the best of our knowledge, it represents the unique hyper logic with a decidable model-checking problem which can express powerful non-regular trace properties when interpreted on singleton sets of traces. We justify the relevance of simple GHyperLTL_SC by showing that it can express diagnosability properties, interesting classes of information-flow security policies, both in the synchronous and asynchronous settings, and bounded termination (more in general, global promptness in the style of Prompt LTL).

cs.LO↗

Predictable and Performant Reactive Synthesis Modulo Theories via Functional Synthesis

Reactive synthesis is the process of generating correct controllers from temporal logic specifications. Classical LTL reactive synthesis handles (propositional) LTL as a specification language. Boolean abstractions allow reducing LTLt specifications (i.e., LTL with propositions replaced by literals from a theory calT), into equi-realizable LTL specifications. In this paper we extend these results into a full static synthesis procedure. The synthesized system receives from the environment valuations of variables from a rich theory calT and outputs valuations of system variables from calT. We use the abstraction method to synthesize a reactive Boolean controller from the LTL specification, and we combine it with functional synthesis to obtain a static controller for the original LTLt specification. We also show that our method allows responses in the sense that the controller can optimize its outputs in order to e.g., always provide the smallest safe values. This is the first full static synthesis method for LTLt, which is a deterministic program (hence predictable and efficient).

cs.LO↗

Fast and Secure Decentralized Optimistic Rollups Using Setchain

Modern blockchains face a scalability challenge due to the intrinsic throughput limitations of consensus protocols. Layer 2 optimistic rollups (L2) are a faster alternative that offer the same interface in terms of smart contract development and user interaction. Optimistic rollups perform most computations offchain and make light use of an underlying blockchain (L1) to guarantee correct behavior, implementing a cheaper blockchain on a blockchain solution. With optimistic rollups, a sequencer calculates offchain batches of L2 transactions and commits batches (compressed or hashed) to the L1 blockchain. The use of hashes requires a data service to translate hashes into their corresponding batches. Current L2 implementations consist of a centralized sequencer (central authority) and an optional data availability committee (DAC). In this paper, we propose a decentralized L2 optimistic rollup based on Setchain, a decentralized Byzantine-tolerant implementation of sets. The main contribution is a fully decentralized "arranger" where arrangers are a formal definition combining sequencers and DACs. We prove our implementation correct and show empirical evidence that our solution scales. A final contribution is a system of incentives (payments) for servers that implement the sequencer and data availability committee protocols correctly, and a fraud-proof mechanism to detect violations of the protocol.

cs.CR↗

Efficient Reactive Synthesis Using Mode Decomposition

Developing critical components, such as mission controllers or embedded systems, is a challenging task. Reactive synthesis is a technique to automatically produce correct controllers. Given a high-level specification written in LTL, reactive synthesis consists of computing a system that satisfies the specification as long as the environment respects the assumptions. Unfortunately, LTL synthesis suffers from high computational complexity which precludes its use for many large cases. A promising approach to improve synthesis scalability consists of decomposing a safety specification into smaller specifications, that can be processed independently and composed into a solution for the original specification. Previous decomposition methods focus on identifying independent parts of the specification whose systems are combined via simultaneous execution. In this work, we propose a novel decomposition algorithm based on modes, which consists of decomposing a complex safety specification into smaller problems whose solution is then composed sequentially (instead of simultaneously). The input to our algorithm is the original specification and the description of the modes. We show how to generate sub-specifications automatically and we prove that if all sub-problems are realizable then the full specification is realizable. Moreover, we show how to construct a system for the original specification from sub-systems for the decomposed specifications. We finally illustrate the feasibility of our approach with multiple case studies using off-the-self synthesis tools to process the obtained sub-problems.

cs.LO↗

Automated Repair of Unrealisable LTL Specifications Guided by Model Counting

The reactive synthesis problem consists of automatically producing correct-by-construction operational models of systems from high-level formal specifications of their behaviours. However, specifications are often unrealisable, meaning that no system can be synthesised from the specification. To deal with this problem, we present AuRUS, a search-based approach to repair unrealisable Linear-Time Temporal Logic (LTL) specifications. AuRUS aims at generating solutions that are similar to the original specifications by using the notions of syntactic and semantic similarities. Intuitively, the syntactic similarity measures the text similarity between the specifications, while the semantic similarity measures the number of behaviours preserved/removed by the candidate repair. We propose a new heuristic based on model counting to approximate semantic similarity. We empirically assess AuRUS on many unrealisable specifications taken from different benchmarks and show that it can successfully repair all of them. Also, compared to related techniques, AuRUS can produce many unique solutions while showing more scalability.

cs.SE↗

Improving Blockchain Scalability with the Setchain Data-type

Blockchain technologies are facing a scalability challenge, which must be overcome to guarantee a wider adoption of the technology. This scalability issue is due to the use of consensus algorithms to guarantee the total order of the chain of blocks and of the transactions within each block. However, total order is often not fully necessary, since important advanced applications of smart-contracts do not require a total order among all operations. A much higher scalability can potentially be achieved if a more relaxed order can be exploited. In this paper, we propose a novel distributed concurrent data type, called Setchain, which improves scalability significantly. A Setchain implements a grow-only set whose elements are not ordered, unlike conventional blockchain operations. When convenient, the Setchain allows forcing a synchronization barrier that assigns permanently an epoch number to a subset of the latest elements added, agreed by consensus. Therefore, two operations in the same epoch are not ordered, while two operations in different epochs are ordered by their respective epoch number. We present different Byzantine-tolerant implementations of Setchain, prove their correctness and report on an empirical evaluation of a prototype implementation. Our results show that Setchain is orders of magnitude faster than consensus-based ledgers, since it implements grow-only sets with epoch synchronization instead of total order. Since Setchain barriers can be synchronized with the underlying blockchain, Setchain objects can be used as a sidechain to implement many decentralized solutions with much faster operations than direct implementations on top of blockchains. Finally, we also present an algorithm that encompasses in a single process the combined behavior of Byzantine servers, which simplifies correctness proofs by encoding the general attacker in a concrete implementation.

cs.DC↗

Decentralized Stream Runtime Verification for Timed Asynchronous Networks

We study the problem of monitoring distributed systems where computers communicate using message passing and share an almost synchronized clock. This is a realistic scenario for networks where the speed of the monitoring is sufficiently slow (at the human scale) to permit efficient clock synchronization, where the clock deviations is small compared to the monitoring cycles. This is the case when monitoring human systems in wide area networks, the Internet or including large deployments. More concretely, we study how to monitor decentralized systems where monitors are expressed as stream runtime verification specifications, under a timed asynchronous network. Our monitors communicate using the network, where messages can take arbitrarily long but cannot be duplicated or lost. This communication setting is common in many cyber-physical systems like smart buildings and ambient living. Previous approaches to decentralized monitoring were limited to synchronous networks, which are not easily implemented in practice because of network failures. Even when networks failures are unusual, they can require several monitoring cycles to be repaired. In this work we propose a solution to the timed asynchronous monitoring problem and show that this problem generalizes the synchronous case. We study the specifications and conditions on the network behavior that allow the monitoring to take place with bounded resources, independently of the trace length. Finally, we report the results of an empirical evaluation of an implementation and verify the theoretical results in terms of effectiveness and efficiency.

cs.LO↗

Efficient Loop Conditions for Bounded Model Checking Hyperproperties

Bounded model checking (BMC) is an effective technique for hunting bugs by incrementally exploring the state space of a system. To reason about infinite traces through a finite structure and to ultimately obtain completeness, BMC incorporates loop conditions that revisit previously observed states. This paper focuses on developing loop conditions for BMC of HyperLTL- a temporal logic for hyperproperties that allows expressing important policies for security and consistency in concurrent systems, etc. Loop conditions for HyperLTL are more complicated than for LTL, as different traces may loop inconsistently in unrelated moments. Existing BMC approaches for HyperLTL only considered linear unrollings without any looping capability, which precludes both finding small infinite traces and obtaining a complete technique. We investigate loop conditions for HyperLTL BMC, where the HyperLTL formula can contain up to one quantifier alternation. We first present a general complete automata-based technique which is based on bounds of maximum unrollings. Then, we introduce alternative simulation-based algorithms that allow exploiting short loops effectively, generating SAT queries whose satisfiability guarantees the outcome of the original model checking problem. We also report empirical evaluation of the prototype implementation of our BMC techniques using Z3py.

cs.LO↗

Bounded Model Checking for Asynchronous Hyperproperties

Many types of attacks on confidentiality stem from the nondeterministic nature of the environment that computer programs operate in (e.g., schedulers and asynchronous communication channels). In this paper, we focus on verification of confidentiality in nondeterministic environments by reasoning about asynchronous hyperproperties. First, we generalize the temporal logic A-HLTL to allow nested trajectory quantification, where a trajectory determines how different execution traces may advance and stutter. We propose a bounded model checking algorithm for A-HLTL based on QBF-solving for a fragment of the generalized A-HLTL and evaluate it by various case studies on concurrent programs, scheduling attacks, compiler optimization, speculative execution, and cache timing attacks. We also rigorously analyze the complexity of model checking for different fragments of A-HLTL.

cs.LO↗

Multi: a Formal Playground for Multi-Smart Contract Interaction

Blockchains are maintained by a network of participants that run algorithms designed to maintain collectively a distributed machine tolerant to Byzantine attacks. From the point of view of users, blockchains provide the illusion of centralized computers that perform trustable verifiable computations, where all computations are deterministic and the results cannot be manipulated or undone. Smart-contracts are written in a special-purpose programming language with deterministic semantics. Each transaction begins with an invocation from an external user to a smart contract. Contracts have local storage and can call other contracts, and more importantly, they store, send and receive cryptocurrency. It is very important to guarantee that contracts are correct before deployment since their code cannot be modified afterward deployment. However, the resulting ecosystem makes it very difficult to reason about program correctness, since contracts can be executed by malicious users or malicious contracts can be designed to exploit other contracts that call them. Many attacks and bugs are caused by unexpected interactions between multiple contracts, the attacked contract and unknown code that performs the exploit. Moreover, there is a very aggressive competition between different blockchains to expand their user base. Ideas are implemented fast and blockchains compete to offer and adopt new features quickly. In this paper, we propose a formal extensible playground that allows reasoning about multi-contract interactions to ultimately prove properties before features are incorporated into the real blockchain. We implemented a model of computation that models the execution platform, abstracts the internal code of each individual contract and focuses on contract interactions. Moreover, we show how many features, existing or proposed, can be used to reason about multi-contract interactions.

cs.LO↗

Setchain: Improving Blockchain Scalability with Byzantine Distributed Sets and Barriers

Blockchain technologies are facing a scalability challenge, which must be overcome to guarantee a wider adoption of the technology. This scalability issue is mostly caused by the use of consensus algorithms to guarantee the total order of the chain of blocks (and of the operations within each block). However, total order is often overkilling, since important advanced applications of smart-contracts do not require a total order of all the operations. Hence, if a more relaxed partial order (instead of a total order) is allowed under certain safety conditions, a much higher scalability can be achieved. In this paper, we propose a distributed concurrent data type, called Setchain, that allows implementing this partial order and increases significantly blockchain scalability. A Setchain implements a grow-only set object whose elements are not totally ordered, unlike conventional blockchain operations. When convenient, the Setchain allows forcing a synchronization barrier that assigns permanently an epoch number to a subset of the latest elements added. With the Setchain, operations in the same epoch are not ordered, while operations in different epochs are. We present different Byzantine-tolerant implementations of Setchain, prove their correctness and report on an empirical evaluation of a direct implementation. Our results show that Setchain is orders of magnitude faster than consensus-based ledgers to implement grow-only sets with epoch synchronization. Since the Setchain barriers can be synchronized with block consolidation, Setchain objects can be used as a sidechain to implement many smart contract solutions with much faster operations than on basic blockchains.

cs.DC↗

A Tableau Method for the Realizability and Synthesis of Reactive Safety Specifications

We introduce a tableau decision method for deciding realizability of specifications expressed in a safety fragment of LTL that includes bounded future temporal operators. Tableau decision procedures for temporal and modal logics have been thoroughly studied for satisfiability and for translating temporal formulae into equivalent Büchi automata, and also for model checking, where a specification and system are provided. However, to the best of our knowledge no tableau method has been studied for the reactive synthesis problem. Reactive synthesis starts from a specification where propositional variables are split into those controlled by the environment and those controlled by the system, and consists on automatically producing a system that guarantees the specification for all environments. Realizability is the decision problem of whether there is one such system. In this paper we present a method to decide realizability of safety specifications, from which we can also extract (i.e. synthesize) a correct system (in case the specification is realizable). Our method can easily be extended to handle richer domains (integers, etc) and bounds in the temporal operators in ways that automata approaches for synthesis cannot.

cs.LO↗