arXiv subjects

João F. Ferreira

Publications and source records attributed to João F. Ferreira.

23 records · Page 2Linked to original sources

arXiv2021

Towards Formal Verification of Password Generation Algorithms used in Password Managers

Password managers are important tools that enable us to use stronger passwords, freeing us from the cognitive burden of remembering them. Despite this, there are still many users who do not fully trust password managers. In this paper, we focus on a feature that most password managers offer that might impact the user's trust, which is the process of generating a random password. We survey which algorithms are most commonly used and we propose a solution for a formally verified reference implementation of a password generation algorithm. We use EasyCrypt as our framework to both specify the reference implementation and to prove its functional correctness and security.

cs.CR↗

arXiv2020

A survey for occultation astrometry of Main Belt: expected astrometric performances

Context: Occultations of stars by asteroids are an efficient method to study the properties of minor bodies, and can be exploited as tools to derive very precise asteroid astrometry relative to the target star. With the availability of stellar astrometry thanks to the ESA mission Gaia, the frequency of good predictions and the quality of the astrometry have been strongly enhanced. Aims: Our goal is to evaluate the astrometric performance of a systematic exploitation of stellar occultations, with a homogeneous data set and a given instrument setup. As a reference instrument, we adopt the example of a robotic 50 cm telescope, which is under construction at the Observatoire de la Côte d Azur. We focus in particular on single chord occultations. Methods: We created a data set of simulated light curves, that are modelled by a Bayesian approach. To build the final statistics, we considered a list of predicted events over a long time span, and stellar astrometry from Gaia data release 2. Results: We derive an acceptable range of observability of the events, with clear indications of the expected errors in terms of timing uncertainties. By converting the distribution of such errors to astrometric uncertainties, we show that the precision on a single chord can reach levels equivalent to the performance of Gaia (sub milli arcseconds). The errors on the asteroid position are dominated by the uncertainty on the position of the occultation chord with respect to the barycentre of the object. Conclusions: The limiting factor in the use of occultation astrometry is not the light curve uncertainty, but our knowledge of the shape and size of the asteroid. This conclusion is valid in a wide range of flux drops and magnitudes of the occulted star. The currently increasing knowledge of the shape, spin properties, and size, must be used to mitigate this source of error.

astro-ph.EP↗

arXiv2020

SmartBugs: A Framework to Analyze Solidity Smart Contracts

Over the last few years, there has been substantial research on automated analysis, testing, and debugging of Ethereum smart contracts. However, it is not trivial to compare and reproduce that research. To address this, we present SmartBugs, an extensible and easy-to-use execution framework that simplifies the execution of analysis tools on smart contracts written in Solidity, the primary language used in Ethereum. SmartBugs is currently distributed with support for 10 tools and two datasets of Solidity contracts. The first dataset can be used to evaluate the precision of analysis tools, as it contains 143 annotated vulnerable contracts with 208 tagged vulnerabilities. The second dataset contains 47,518 unique contracts collected through Etherscan. We discuss how SmartBugs supported the largest experimental setup to date both in the number of tools and in execution time. Moreover, we show how it enables easy integration and comparison of analysis tools by presenting a new extension to the tool SmartCheck that improves substantially the detection of vulnerabilities related to the DASP10 categories Bad Randomness, Time Manipulation, and Access Control (identified vulnerabilities increased from 11% to 24%).

cs.SE↗

arXiv2020

Empirical Review of Automated Analysis Tools on 47,587 Ethereum Smart Contracts

Over the last few years, there has been substantial research on automated analysis, testing, and debugging of Ethereum smart contracts. However, it is not trivial to compare and reproduce that research. To address this, we present an empirical evaluation of 9 state-of-the-art automated analysis tools using two new datasets: i) a dataset of 69 annotated vulnerable smart contracts that can be used to evaluate the precision of analysis tools; and ii) a dataset with all the smart contracts in the Ethereum Blockchain that have Solidity source code available on Etherscan (a total of 47,518 contracts). The datasets are part of SmartBugs, a new extendable execution framework that we created to facilitate the integration and comparison between multiple analysis tools and the analysis of Ethereum smart contracts. We used SmartBugs to execute the 9 automated analysis tools on the two datasets. In total, we ran 428,337 analyses that took approximately 564 days and 3 hours, being the largest experimental setup to date both in the number of tools and in execution time. We found that only 42% of the vulnerabilities from our annotated dataset are detected by all the tools, with the tool Mythril having the higher accuracy (27%). When considering the largest dataset, we observed that 97% of contracts are tagged as vulnerable, thus suggesting a considerable number of false positives. Indeed, only a small number of vulnerabilities (and of only two categories) were detected simultaneously by four or more tools.

cs.SE↗

arXiv2015

On Euclid's Algorithm and Elementary Number Theory

Algorithms can be used to prove and to discover new theorems. This paper shows how algorithmic skills in general, and the notion of invariance in particular, can be used to derive many results from Euclid's algorithm. We illustrate how to use the algorithm as a verification interface (i.e., how to verify theorems) and as a construction interface (i.e., how to investigate and derive new theorems). The theorems that we verify are well-known and most of them are included in standard number theory books. The new results concern distributivity properties of the greatest common divisor and a new algorithm for efficiently enumerating the positive rationals in two different ways. One way is known and is due to Moshe Newman. The second is new and corresponds to a deforestation of the Stern-Brocot tree of rationals. We show that both enumerations stem from the same simple algorithm. In this way, we construct a Stern-Brocot enumeration algorithm with the same time and space complexity as Newman's algorithm. A short review of the original papers by Stern and Brocot is also included.

cs.DS↗