BZPEERReading, trust and collaboration for research
Menu

Discover

GraphFollow connections around a paper, topic or saved view.

Workspaces

HomePick up where your research flow left off.InboxHandle requests, replies and notifications from one place.CollectionsCurate reading lists, evidence sets and shareable dossiers.ResearchSee your private provenance graph, trail and imports.CollaborationMove from discovery into focused discussion rooms.PublishDraft, preview and publish full-text research articles.

Network

ExpertsFind specialists worth following or asking for help.CommunitiesJoin research circles organized around shared work.PartnersSee external organizations active around the same topics.

Opportunities

ListingsBrowse roles, calls and collaborations with clearer fit signals.

Account

Log inReturn to your reading and collaboration workspace.Create accountStart saving work, following people and joining teams.
Log inCreate account

Researcher profile

João F. Ferreira

João F. Ferreira contributes to research discovery and scholarly infrastructure.

ResearcherAffiliation not importedOpen to collaborate
Software Engineeringastro-ph.EPastro-ph.IMCryptography and Securityastro-ph.SRLogic in Computer ScienceProgramming Languages

Trust snapshot

Quick read

Trust 21 - Emerging
6works
0followers
7topics
4close collaborators

Actions

Decide how to stay connected

Follow researcher0

Research graph

See the researcher in context

Open full explorer

Inspect adjacent work, topics, institutions and collaborators without jumping out to a separate graph page.

Building this graph slice

BZPEER is loading the nearby papers, people, topics and institutions for this page.

Published work

6 published item(s)

preprint2024arXiv

Leveraging Large Language Models to Boost Dafny's Developers Productivity

This research idea paper proposes leveraging Large Language Models (LLMs) to enhance the productivity of Dafny developers. Although the use of verification-aware languages, such as Dafny, has increased considerably in the last decade, these are still not widely adopted. Often the cost of using such languages is too high, due to the level of expertise required from the developers and challenges that they often face when trying to prove a program correct. Even though Dafny automates a lot of the verification process, sometimes there are steps that are too complex for Dafny to perform on its own. One such case is that of missing lemmas, i.e. Dafny is unable to prove a result without being given further help in the form of a theorem that can assist it in the proof of the step. In this paper, we describe preliminary work on a new Dafny plugin that leverages LLMs to assist developers by generating suggestions for relevant lemmas that Dafny is unable to discover and use. Moreover, for the lemmas that cannot be proved automatically, the plugin also attempts to provide accompanying calculational proofs. We also discuss ideas for future work by describing a research agenda on using LLMs to increase the adoption of verification-aware languages in general, by increasing developers productivity and by reducing the level of expertise required for crafting formal specifications and proving program properties.

0 citations0 reviewsNo code linkedOpen access
preprint2022arXiv

Asteroid astrometry by stellar occultations: Accuracy of the existing sample from orbital fitting

Context: Stellar occultations, greatly enhanced by the publication of the Gaia data releases, permit not only the determination of asteroid size and shape, but also the retrieval of additional, accurate astrometry, with a possible relevant impact on the study of dynamical properties. The use of Gaia as reference catalogue and the recent implementation of an improved error model for occultation astrometry offer the opportunity to test its global astrometric performance on the existing data set of observed events, dominated by minor planets belonging to the main belt. Aims: We aim to explore the performance on orbit accuracy brought by reducing occultations by stellar positions given in Gaia Data Release 2 (DR2) and Early Data Release 3 (EDR3), exploited jointly with the new occultation error model. Our goal is to verify that the quality of DR2 and EDR3 provides a logical progression in the exploitation of occultation astrometry with respect to previous catalogues. We also want to compare the post-fit residuals to the error model. Methods: We began with accurate orbit adjustment to occultation data, either alone or joined to the other available ground-based observations. We then analyzed the orbit accuracy and the post-fit residuals. Results: Gaia EDR3 and DR2 bring a noticeable improvement to the accuracy of occultation data, bringing an average reduction of their residuals upon fitting an orbit of about a factor of 5 when compared to other catalogues. This is particularly visible when occultations alone are used, resulting in very good orbits for a large fraction of objects. We demonstrate that occultation astrometry can reach the performance of Gaia on small asteroids. The joint use of archival data and occultations remains more challenging due to the higher uncertainties and systematic errors of other data, mainly obtained by traditional CCD imaging.

0 citations0 reviewsNo code linkedOpen access
preprint2022arXiv

GLITCH: Automated Polyglot Security Smell Detection in Infrastructure as Code

Infrastructure as Code (IaC) is the process of managing IT infrastructure via programmable configuration files (also called IaC scripts). Like other software artifacts, IaC scripts may contain security smells, which are coding patterns that can result in security weaknesses. Automated analysis tools to detect security smells in IaC scripts exist, but they focus on specific technologies such as Puppet, Ansible, or Chef. This means that when the detection of a new smell is implemented in one of the tools, it is not immediately available for the technologies supported by the other tools -- the only option is to duplicate the effort. This paper presents an approach that enables consistent security smell detection across different IaC technologies. We conduct a large-scale empirical study that analyzes security smells on three large datasets containing 196,755 IaC scripts and 12,281,251 LOC. We show that all categories of security smells are identified across all datasets and we identify some smells that might affect many IaC projects. To conduct this study, we developed GLITCH, a new technology-agnostic framework that enables automated polyglot smell detection by transforming IaC scripts into an intermediate representation, on which different security smell detectors can be defined. GLITCH currently supports the detection of nine different security smells in scripts written in Ansible, Chef, or Puppet. We compare GLITCH with state-of-the-art security smell detectors. The results obtained not only show that GLITCH can reduce the effort of writing security smell analyses for multiple IaC technologies, but also that it has higher precision and recall than the current state-of-the-art tools.

0 citations0 reviewsNo code linkedOpen access
preprint2020arXiv

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.

0 citations0 reviewsNo code linkedOpen access
preprint2020arXiv

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.

0 citations0 reviewsNo code linkedOpen access
preprint2020arXiv

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%).

0 citations0 reviewsNo code linkedOpen access