arXiv subjects

Maximiliano Cristiá

Publications and source records attributed to Maximiliano Cristiá.

25 records · Page 2Linked to original sources

arXiv2020

An Automatically Verified Prototype of the Tokeneer ID Station Specification

The Tokeneer project was an initiative set forth by the National Security Agency (NSA, USA) to be used as a demonstration that developing highly secure systems can be made by applying rigorous methods in a cost effective manner. Altran Praxis (UK) was selected by NSA to carry out the development of the Tokeneer ID Station. The company wrote a Z specification later implemented in the SPARK Ada programming language, which was verified using the SPARK Examiner toolset. In this paper, we show that the Z specification can be easily and naturally encoded in the {log} set constraint language, thus generating a functional prototype. Furthermore, we show that {log}'s automated proving capabilities can discharge all the proof obligations concerning state invariants as well as important security properties. As a consequence, the prototype can be regarded as correct with respect to the verified properties. This provides empirical evidence that Z users can use {log} to generate correct prototypes from their Z specifications. In turn, these prototypes enable or simplify some verificatio activities discussed in the paper.

cs.SE↗

arXiv2020

Declarative Programming with Intensional Sets in Java Using JSetL

Intensional sets are sets given by a property rather than by enumerating their elements. In previous work, we have proposed a decision procedure for a first-order logic language which provides Restricted Intensional Sets (RIS), i.e., a sub-class of intensional sets that are guaranteed to denote finite---though unbounded---sets. In this paper we show how RIS can be exploited as a convenient programming tool also in a conventional setting, namely, the imperative O-O language Java. We do this by considering a Java library, called JSetL, that integrates the notions of logical variable, (set) unification and constraints that are typical of constraint logic programming languages into the Java language. We show how JSetL is naturally extended to accommodate for RIS and RIS constraints, and how this extension can be exploited, on the one hand, to support a more declarative style of programming and, on the other hand, to effectively enhance the expressive power of the constraint language provided by the library.

cs.PL↗

arXiv2019

Automated Reasoning with Restricted Intensional Sets

Intensional sets, i.e., sets given by a property rather than by enumerating elements, are widely recognized as a key feature to describe complex problems (see, e.g., specification languages such as B and Z). Notwithstanding, very few tools exist supporting high-level automated reasoning on general formulas involving intensional sets. In this paper we present a decision procedure for a first-order logic language offering both extensional and (a restricted form of) intensional sets (RIS). RIS are introduced as first-class citizens of the language and set-theoretical operators on RIS are dealt with as constraints. Syntactic restrictions on RIS guarantee that the denoted sets are finite, though unbounded. The language of RIS, called L_RIS , is parametric with respect to any first-order theory X providing at least equality and a decision procedure for X-formulas. In particular, we consider the instance of L_RIS when X is the theory of hereditarily finite sets and binary relations. We also present a working implementation of this instance as part of the {log} tool and we show through a number of examples and two case studies that, although RIS are a subclass of general intensional sets, they are still sufficiently expressive as to encode and solve many interesting problems. Finally, an extensive empirical evaluation provides evidence that the tool can be used in practice.

cs.LO↗

arXiv2019

Set-Based Models for Cryptocurrency Software

Emin Gün Sirer once said: It's clear that writing a robust, secure smart contract requires extreme amounts of diligence. It's more similar to writing code for a nuclear power reactor, than to writing loose web code [...] Yet the current Solidity language and underlying EVM seems designed more for the latter. Formal methods (FM) are mathematics-based software development methods aimed at producing "code for a nuclear power reactor". That is, due application of FM can produce bug-free, zero-defect, correct-by-construction, guaranteed, certified software. However, the software industry seldom use FM. One of the main reasons for such a situation is that there exists the perception (which might well be a fact) that FM increase software costs. On the other hand, FM can be partially applied thus producing high-quality software, although not necessarily bug-free. In this paper we outline some FM related techniques whose application the cryptocurrency community should take into consideration because they could bridge the gap between "loose web code" and "code for a nuclear power reactor".

cs.SE↗

arXiv2019

Towards a formally verified implementation of the MimbleWimble cryptocurrency protocol

MimbleWimble is a privacy-oriented cryptocurrency technology encompassing security and scalability properties that distinguish it from other protocols of the kind. In this paper we present and briefly discuss those properties and outline the basis of a model-driven verification approach to address the certification of the correctness of a particular implementation of the protocol.

cs.CR↗

arXiv2014

A Family of Simulation Criteria to Guide DEVS Models Validation Rigorously, Systematically and Semi-Automatically

The most common method to validate a DEVS model against the requirements is to simulate it several times under different conditions, with some simulation tool. The behavior of the model is compared with what the system is supposed to do. The number of different scenarios to simulate is usually infinite, therefore, selecting them becomes a crucial task. This selection, actually, is made following the experience or intuition of an engineer. Here we present a family of criteria to conduct DEVS model simulations in a disciplined way and covering the most significant simulations to increase the confidence on the model. This is achieved by analyzing the mathematical representation of the DEVS model and, thus, part of the validation process can be automatized.

cs.SE↗

arXiv2012

Applying SMT Solvers to the Test Template Framework

The Test Template Framework (TTF) is a model-based testing method for the Z notation. In the TTF, test cases are generated from test specifications, which are predicates written in Z. In turn, the Z notation is based on first-order logic with equality and Zermelo-Fraenkel set theory. In this way, a test case is a witness satisfying a formula in that theory. Satisfiability Modulo Theory (SMT) solvers are software tools that decide the satisfiability of arbitrary formulas in a large number of built-in logical theories and their combination. In this paper, we present the first results of applying two SMT solvers, Yices and CVC3, as the engines to find test cases from TTF's test specifications. In doing so, shallow embeddings of a significant portion of the Z notation into the input languages of Yices and CVC3 are provided, given that they do not directly support Zermelo-Fraenkel set theory as defined in Z. Finally, the results of applying these embeddings to a number of test specifications of eight cases studies are analysed.

cs.SE↗