Showing 1–14 of 14 results for author: Ceresa, M

Fast and Secure Decentralized Optimistic Rollups Using Setchain

Authors: Margarita Capretto, Martín Ceresa, Antonio Fernández Anta, Pedro Moreno-Sánchez, César Sánchez

Abstract: 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,… ▽ More 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. △ Less

Submitted 4 June, 2024; originally announced June 2024.

Monitoring the Future of Smart Contracts

Authors: Margarita Capretto, Martin Ceresa, Cesar Sanchez

Abstract: Blockchains are decentralized systems that provide trustable execution guarantees. Smart contracts are programs written in specialized programming languages running on blockchains that govern how tokens and cryptocurrency are sent and received. Smart contracts can invoke other smart contracts during the execution of transactions always initiated by external users. Once deployed, smart contracts… ▽ More Blockchains are decentralized systems that provide trustable execution guarantees. Smart contracts are programs written in specialized programming languages running on blockchains that govern how tokens and cryptocurrency are sent and received. Smart contracts can invoke other smart contracts during the execution of transactions always initiated by external users. Once deployed, smart contracts cannot be modified, so techniques like runtime verification are very appealing for improving their reliability. However, the conventional model of computation of smart contracts is transactional: once operations commit, their effects are permanent and cannot be undone. In this paper, we proposed the concept of future monitors which allows monitors to remain waiting for future transactions to occur before committing or aborting. This is inspired by optimistic rollups, which are modern blockchain implementations that increase efficiency (and reduce cost) by delaying transaction effects. We exploit this delay to propose a model of computation that allows (bounded) future monitors. We show our monitors correct respect of legacy transactions, how they implement future bounded monitors and how they guarantee progress. We illustrate the use of future bounded monitors to implement correctly multi-transaction flash loans. △ Less

Submitted 22 January, 2024; originally announced January 2024.

Unsupervised Segmentation of Fetal Brain MRI using Deep Learning Cascaded Registration

Authors: Valentin Comte, Mireia Alenya, Andrea Urru, Judith Recober, Ayako Nakaki, Francesca Crovetto, Oscar Camara, Eduard Gratacós, Elisenda Eixarch, Fàtima Crispi, Gemma Piella, Mario Ceresa, Miguel A. González Ballester

Abstract: Accurate segmentation of fetal brain magnetic resonance images is crucial for analyzing fetal brain development and detecting potential neurodevelopmental abnormalities. Traditional deep learning-based automatic segmentation, although effective, requires extensive training data with ground-truth labels, typically produced by clinicians through a time-consuming annotation process. To overcome this… ▽ More Accurate segmentation of fetal brain magnetic resonance images is crucial for analyzing fetal brain development and detecting potential neurodevelopmental abnormalities. Traditional deep learning-based automatic segmentation, although effective, requires extensive training data with ground-truth labels, typically produced by clinicians through a time-consuming annotation process. To overcome this challenge, we propose a novel unsupervised segmentation method based on multi-atlas segmentation, that accurately segments multiple tissues without relying on labeled data for training. Our method employs a cascaded deep learning network for 3D image registration, which computes small, incremental deformations to the moving image to align it precisely with the fixed image. This cascaded network can then be used to register multiple annotated images with the image to be segmented, and combine the propagated labels to form a refined segmentation. Our experiments demonstrate that the proposed cascaded architecture outperforms the state-of-the-art registration methods that were tested. Furthermore, the derived segmentation method achieves similar performance and inference time to nnU-Net while only using a small subset of annotated data for the multi-atlas segmentation task and none for training the network. Our pipeline for registration and multi-atlas segmentation is publicly available at https://github.com/ValBcn/CasReg. △ Less

Submitted 7 July, 2023; originally announced July 2023.

Comments: 17 pages, 8 figures, 5 tables, paper submitted to IEEE transaction on medical imaging

Improving Blockchain Scalability with the Setchain Data-type

Authors: Margarita Capretto, Martín Ceresa, Antonio Fernández Anta, Antonio Russo, César Sánchez

Abstract: 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… ▽ More 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. △ Less

Submitted 9 February, 2023; originally announced February 2023.

Comments: 32 pages 6 figures. arXiv admin note: substantial text overlap with arXiv:2206.11845

Multi: a Formal Playground for Multi-Smart Contract Interaction

Authors: Martán Ceresa, César Sánchez

Abstract: 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-co… ▽ More 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. △ Less

Submitted 14 July, 2022; originally announced July 2022.

Transaction Monitoring of Smart Contracts

Authors: Margarita Capretto, Martin Ceresa, Cesar Sanchez

Abstract: Blockchains are modern distributed systems that provide decentralized financial capabilities with trustable guarantees. Smart contracts are programs written in specialized programming languages running on a blockchain and govern how tokens and cryptocurrency are sent and received. Smart contracts can invoke other contracts during the execution of transactions initiated by external users. Once de… ▽ More Blockchains are modern distributed systems that provide decentralized financial capabilities with trustable guarantees. Smart contracts are programs written in specialized programming languages running on a blockchain and govern how tokens and cryptocurrency are sent and received. Smart contracts can invoke other contracts during the execution of transactions initiated by external users. Once deployed, smart contracts cannot be modified and their pitfalls can cause malfunctions and losses, for example by attacks from malicious users. Runtime verification is a very appealing technique to improve the reliability of smart contracts. One approach consists of specifying undesired executions (never claims) and detecting violations of the specification on the fly. This can be done by extending smart contracts with additional instructions corresponding to monitor specified properties, resulting in an onchain monitoring approach. In this paper, we study transaction monitoring that consists of detecting violations of complete transaction executions and not of individual operations within transactions. Our main contributions are to show that transaction monitoring is not possible in most blockchains and propose different execution mechanisms that would enable transaction monitoring. △ Less

Submitted 6 July, 2022; originally announced July 2022.

Setchain: Improving Blockchain Scalability with Byzantine Distributed Sets and Barriers

Authors: Margarita Capretto, Martín Ceresa, Antonio Fernández Anta, Antonio Russo, César Sánchez

Abstract: 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-contract… ▽ More 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. △ Less

Submitted 23 June, 2022; originally announced June 2022.

An Uncertainty-aware Hierarchical Probabilistic Network for Early Prediction, Quantification and Segmentation of Pulmonary Tumour Growth

Authors: Xavier Rafael-Palou, Anton Aubanell, Mario Ceresa, Vicent Ribas, Gemma Piella, Miguel A. González Ballester

Abstract: Early detection and quantification of tumour growth would help clinicians to prescribe more accurate treatments and provide better surgical planning. However, the multifactorial and heterogeneous nature of lung tumour progression hampers identification of growth patterns. In this study, we present a novel method based on a deep hierarchical generative and probabilistic framework that, according to… ▽ More Early detection and quantification of tumour growth would help clinicians to prescribe more accurate treatments and provide better surgical planning. However, the multifactorial and heterogeneous nature of lung tumour progression hampers identification of growth patterns. In this study, we present a novel method based on a deep hierarchical generative and probabilistic framework that, according to radiological guidelines, predicts tumour growth, quantifies its size and provides a semantic appearance of the future nodule. Unlike previous deterministic solutions, the generative characteristic of our approach also allows us to estimate the uncertainty in the predictions, especially important for complex and doubtful cases. Results of evaluating this method on an independent test set reported a tumour growth balanced accuracy of 74%, a tumour growth size MAE of 1.77 mm and a tumour segmentation Dice score of 78%. These surpassed the performances of equivalent deterministic and alternative generative solutions (i.e. probabilistic U-Net, Bayesian test dropout and Pix2Pix GAN) confirming the suitability of our approach. △ Less

Submitted 18 April, 2021; originally announced April 2021.

Comments: 24 pages, 9 figures

MSC Class: 68T07; 68T35 ACM Class: I.5.2; I.4.0; I.2.1; I.2.6

Detection, growth quantification and malignancy prediction of pulmonary nodules using deep convolutional networks in follow-up CT scans

Authors: Xavier Rafael-Palou, Anton Aubanell, Mario Ceresa, Vicent Ribas, Gemma Piella, Miguel A. González Ballester

Abstract: We address the problem of supporting radiologists in the longitudinal management of lung cancer. Therefore, we proposed a deep learning pipeline, composed of four stages that completely automatized from the detection of nodules to the classification of cancer, through the detection of growth in the nodules. In addition, the pipeline integrated a novel approach for nodule growth detection, which re… ▽ More We address the problem of supporting radiologists in the longitudinal management of lung cancer. Therefore, we proposed a deep learning pipeline, composed of four stages that completely automatized from the detection of nodules to the classification of cancer, through the detection of growth in the nodules. In addition, the pipeline integrated a novel approach for nodule growth detection, which relied on a recent hierarchical probabilistic U-Net adapted to report uncertainty estimates. Also, a second novel method was introduced for lung cancer nodule classification, integrating into a two stream 3D-CNN network the estimated nodule malignancy probabilities derived from a pretrained nodule malignancy network. The pipeline was evaluated in a longitudinal cohort and reported comparable performances to the state of art. △ Less

Submitted 26 March, 2021; originally announced March 2021.

MSC Class: 65D19; 68T10 ACM Class: I.3; I.4

Pulmonary Nodule Malignancy Classification Using its Temporal Evolution with Two-Stream 3D Convolutional Neural Networks

Authors: Xavier Rafael-Palou, Anton Aubanell, Ilaria Bonavita, Mario Ceresa, Gemma Piella, Vicent Ribas, Miguel A. González Ballester

Abstract: Nodule malignancy assessment is a complex, time-consuming and error-prone task. Current clinical practice requires measuring changes in size and density of the nodule at different time-points. State of the art solutions rely on 3D convolutional neural networks built on pulmonary nodules obtained from single CT scan per patient. In this work, we propose a two-stream 3D convolutional neural network… ▽ More Nodule malignancy assessment is a complex, time-consuming and error-prone task. Current clinical practice requires measuring changes in size and density of the nodule at different time-points. State of the art solutions rely on 3D convolutional neural networks built on pulmonary nodules obtained from single CT scan per patient. In this work, we propose a two-stream 3D convolutional neural network that predicts malignancy by jointly analyzing two pulmonary nodule volumes from the same patient taken at different time-points. Best results achieve 77% of F1-score in test with an increment of 9% and 12% of F1-score with respect to the same network trained with images from a single time-point. △ Less

Submitted 22 May, 2020; originally announced May 2020.

Report number: MIDL/2020/ExtendedAbstract/D1jTt_FOPY

Declarative Stream Runtime Verification (hLola)

Authors: Martin Ceresa, Felipe Gorostiaga, Cesar Sanchez

Abstract: Stream Runtime Verification is a formal dynamic analysis technique that generalizes runtime verification algorithms from temporal logics like LTL to stream monitoring, allowing to compute richer verdicts than Booleans (including quantitative and arbitrary data). In this paper we study the problem of implementing an SRV engine that is truly extensible to arbitrary data theories, and we propose a so… ▽ More Stream Runtime Verification is a formal dynamic analysis technique that generalizes runtime verification algorithms from temporal logics like LTL to stream monitoring, allowing to compute richer verdicts than Booleans (including quantitative and arbitrary data). In this paper we study the problem of implementing an SRV engine that is truly extensible to arbitrary data theories, and we propose a solution as a Haskell embedded domain specific language. In spite of the theoretical clean separation in SRV between temporal dependencies and data computations, previous engines include ad-hoc implementations of a few data types, requiring complex changes to incorporate new data theories. We propose here an SRV language called hLola that borrows general Haskell types and embeds them transparently into an eDSL. This novel technique, which we call lift deep embedding, allows for example, the use of higher-order functions for static stream parameterization. We describe the Haskell implementation of hLola and illustrate simple extensions implemented using libraries, which require long and error-prone additions in other ad-hoc SRV formalisms. △ Less

Submitted 3 September, 2020; v1 submitted 28 February, 2020; originally announced March 2020.

Comments: 21 pages, 1 figure

Re-Identification and Growth Detection of Pulmonary Nodules without Image Registration Using 3D Siamese Neural Networks

Authors: Xavier Rafael-Palou, Anton Aubanell, Ilaria Bonavita, Mario Ceresa, Gemma Piella, Vicent Ribas, Miguel Ángel González Ballester

Abstract: Lung cancer follow-up is a complex, error prone, and time consuming task for clinical radiologists. Several lung CT scan images taken at different time points of a given patient need to be individually inspected, looking for possible cancerogenous nodules. Radiologists mainly focus their attention in nodule size, density, and growth to assess the existence of malignancy. In this study, we present… ▽ More Lung cancer follow-up is a complex, error prone, and time consuming task for clinical radiologists. Several lung CT scan images taken at different time points of a given patient need to be individually inspected, looking for possible cancerogenous nodules. Radiologists mainly focus their attention in nodule size, density, and growth to assess the existence of malignancy. In this study, we present a novel method based on a 3D siamese neural network, for the re-identification of nodules in a pair of CT scans of the same patient without the need for image registration. The network was integrated into a two-stage automatic pipeline to detect, match, and predict nodule growth given pairs of CT scans. Results on an independent test set reported a nodule detection sensitivity of 94.7%, an accuracy for temporal nodule matching of 88.8%, and a sensitivity of 92.0% with a precision of 88.4% for nodule growth detection. △ Less

Submitted 22 December, 2019; originally announced December 2019.

Comments: 14 pages, 8 figures

Integration of Convolutional Neural Networks for Pulmonary Nodule Malignancy Assessment in a Lung Cancer Classification Pipeline

Authors: Ilaria Bonavita, Xavier Rafael-Palou, Mario Ceresa, Gemma Piella, Vicent Ribas, Miguel A. González Ballester

Abstract: The early identification of malignant pulmonary nodules is critical for better lung cancer prognosis and less invasive chemo or radio therapies. Nodule malignancy assessment done by radiologists is extremely useful for planning a preventive intervention but is, unfortunately, a complex, time-consuming and error-prone task. This explains the lack of large datasets containing radiologists malignancy… ▽ More The early identification of malignant pulmonary nodules is critical for better lung cancer prognosis and less invasive chemo or radio therapies. Nodule malignancy assessment done by radiologists is extremely useful for planning a preventive intervention but is, unfortunately, a complex, time-consuming and error-prone task. This explains the lack of large datasets containing radiologists malignancy characterization of nodules. In this article, we propose to assess nodule malignancy through 3D convolutional neural networks and to integrate it in an automated end-to-end existing pipeline of lung cancer detection. For training and testing purposes we used independent subsets of the LIDC dataset. Adding the probabilities of nodules malignity in a baseline lung cancer pipeline improved its F1-weighted score by 14.7%, whereas integrating the malignancy model itself using transfer learning outperformed the baseline prediction by 11.8% of F1-weighted score. Despite the limited size of the lung cancer datasets, integrating predictive models of nodule malignancy improves prediction of lung cancer. △ Less

Submitted 18 December, 2019; originally announced December 2019.

Comments: 26 pages, 5 figures

Journal ref: Computer Methods and Programs in Biomedicine, volume=185,number=105172, pages=1-9, year=2019, publisher=Elsevier

Fully automatic detection and segmentation of abdominal aortic thrombus in post-operative CTA images using deep convolutional neural networks

Authors: Karen López-Linares, Nerea Aranjuelo, Luis Kabongo, Gregory Maclair, Nerea Lete, Mario Ceresa, Ainhoa García-Familiar, Iván Macía, Miguel A. González Ballester

Abstract: Computerized Tomography Angiography (CTA) based follow-up of Abdominal Aortic Aneurysms (AAA) treated with Endovascular Aneurysm Repair (EVAR) is essential to evaluate the progress of the patient and detect complications. In this context, accurate quantification of post-operative thrombus volume is required. However, a proper evaluation is hindered by the lack of automatic, robust and reproducible… ▽ More Computerized Tomography Angiography (CTA) based follow-up of Abdominal Aortic Aneurysms (AAA) treated with Endovascular Aneurysm Repair (EVAR) is essential to evaluate the progress of the patient and detect complications. In this context, accurate quantification of post-operative thrombus volume is required. However, a proper evaluation is hindered by the lack of automatic, robust and reproducible thrombus segmentation algorithms. We propose a new fully automatic approach based on Deep Convolutional Neural Networks (DCNN) for robust and reproducible thrombus region of interest detection and subsequent fine thrombus segmentation. The DetecNet detection network is adapted to perform region of interest extraction from a complete CTA and a new segmentation network architecture, based on Fully Convolutional Networks and a Holistically-Nested Edge Detection Network, is presented. These networks are trained, validated and tested in 13 post-operative CTA volumes of different patients using a 4-fold cross-validation approach to provide more robustness to the results. Our pipeline achieves a Dice score of more than 82% for post-operative thrombus segmentation and provides a mean relative volume difference between ground truth and automatic segmentation that lays within the experienced human observer variance without the need of human intervention in most common cases. △ Less

Submitted 1 April, 2018; originally announced April 2018.