Showing 1–10 of 10 results for author: Pereira, J C

Protocols to Code: Formal Verification of a Next-Generation Internet Router

Authors: João C. Pereira, Tobias Klenze, Sofia Giampietro, Markus Limbeck, Dionysios Spiliopoulos, Felix A. Wolf, Marco Eilers, Christoph Sprenger, David Basin, Peter Müller, Adrian Perrig

Abstract: We present the first formally-verified Internet router, which is part of the SCION Internet architecture. SCION routers run a cryptographic protocol for secure packet forwarding in an adversarial environment. We verify both the protocol's network-wide security properties and low-level properties of its implementation. More precisely, we develop a series of protocol models by refinement in Isabelle… ▽ More We present the first formally-verified Internet router, which is part of the SCION Internet architecture. SCION routers run a cryptographic protocol for secure packet forwarding in an adversarial environment. We verify both the protocol's network-wide security properties and low-level properties of its implementation. More precisely, we develop a series of protocol models by refinement in Isabelle/HOL and we use an automated program verifier to prove that the router's Go code satisfies memory safety, crash freedom, freedom from data races, and adheres to the protocol model. Both verification efforts are soundly linked together. Our work demonstrates the feasibility of coherently verifying a critical network component from high-level protocol models down to performance-optimized production code, developed by an independent team. In the process, we uncovered critical bugs in both the protocol and its implementation, which were confirmed by the code developers, and we strengthened the protocol's security properties. This paper explains our approach, summarizes the main results, and distills lessons for the design and implementation of verifiable systems, for the handling of continuous changes, and for the verification techniques and tools employed. △ Less

Submitted 9 May, 2024; originally announced May 2024.

Refinement Proofs in Rust Using Ghost Locks

Authors: Aurel Bílý, João C. Pereira, Jan Schär, Peter Müller

Abstract: Refinement transforms an abstract system model into a concrete, executable program, such that properties established for the abstract model carry over to the concrete implementation. Refinement has been used successfully in the development of substantial verified systems. Nevertheless, existing refinement techniques have limitations that impede their practical usefulness. Some techniques generate… ▽ More Refinement transforms an abstract system model into a concrete, executable program, such that properties established for the abstract model carry over to the concrete implementation. Refinement has been used successfully in the development of substantial verified systems. Nevertheless, existing refinement techniques have limitations that impede their practical usefulness. Some techniques generate executable code automatically, which generally leads to implementations with sub-optimal performance. Others employ bottom-up program verification to reason about efficient implementations, but impose strict requirements on the structure of the code, the structure of the refinement proofs, as well as the employed verification logic and tools. In this paper, we present a novel refinement technique that removes these limitations. It supports a wide range of program structures, data representations, and proof structures. Our approach supports reasoning about both safety and liveness properties. We implement our approach in a state-of-the-art verifier for the Rust language, which itself offers a strong foundation for memory safety. We demonstrate the practicality of our approach on a number of substantial case studies. △ Less

Submitted 24 November, 2023; originally announced November 2023.

Comments: 21 pages, 3 figures, submitted to PLDI 2024

MSC Class: 68Q60 ACM Class: F.3.1

Content-Diverse Comparisons improve IQA

Authors: William Thong, Jose Costa Pereira, Sarah Parisot, Ales Leonardis, Steven McDonagh

Abstract: Image quality assessment (IQA) forms a natural and often straightforward undertaking for humans, yet effective automation of the task remains highly challenging. Recent metrics from the deep learning community commonly compare image pairs during training to improve upon traditional metrics such as PSNR or SSIM. However, current comparisons ignore the fact that image content affects quality assessm… ▽ More Image quality assessment (IQA) forms a natural and often straightforward undertaking for humans, yet effective automation of the task remains highly challenging. Recent metrics from the deep learning community commonly compare image pairs during training to improve upon traditional metrics such as PSNR or SSIM. However, current comparisons ignore the fact that image content affects quality assessment as comparisons only occur between images of similar content. This restricts the diversity and number of image pairs that the model is exposed to during training. In this paper, we strive to enrich these comparisons with content diversity. Firstly, we relax comparison constraints, and compare pairs of images with differing content. This increases the variety of available comparisons. Secondly, we introduce listwise comparisons to provide a holistic view to the model. By including differentiable regularizers, derived from correlation coefficients, models can better adjust predicted scores relative to one another. Evaluation on multiple benchmarks, covering a wide range of distortions and image content, shows the effectiveness of our learning scheme for training image quality assessment models. △ Less

Submitted 9 November, 2022; originally announced November 2022.

Comments: Accepted at British Machine Vision Conference (BMVC) 2022

Gobra: Modular Specification and Verification of Go Programs (extended version)

Authors: Felix A. Wolf, Linard Arquint, Martin Clochard, Wytse Oortwijn, João C. Pereira, Peter Müller

Abstract: Go is an increasingly-popular systems programming language targeting, especially, concurrent and distributed systems. Go differentiates itself from other imperative languages by offering structural subty** and lightweight concurrency through goroutines with message-passing communication. This combination of features poses interesting challenges for static verification, most prominently the combi… ▽ More Go is an increasingly-popular systems programming language targeting, especially, concurrent and distributed systems. Go differentiates itself from other imperative languages by offering structural subty** and lightweight concurrency through goroutines with message-passing communication. This combination of features poses interesting challenges for static verification, most prominently the combination of a mutable heap and advanced concurrency primitives. We present Gobra, a modular, deductive program verifier for Go that proves memory safety, crash safety, data-race freedom, and user-provided specifications. Gobra is based on separation logic and supports a large subset of Go. Its implementation translates an annotated Go program into the Viper intermediate verification language and uses an existing SMT-based verification backend to compute and discharge proof obligations. △ Less

Submitted 28 May, 2021; originally announced May 2021.

NTIRE 2021 Challenge on Perceptual Image Quality Assessment

Authors: **** Gu, Haoming Cai, Chao Dong, Jimmy S. Ren, Yu Qiao, Shuhang Gu, Radu Timofte, Manri Cheon, Sungjun Yoon, Byungyeon Kang, Junwoo Lee, Qing Zhang, Haiyang Guo, Yi Bin, Yuqing Hou, Hengliang Luo, **gyu Guo, Zirui Wang, Hai Wang, Wenming Yang, Qingyan Bai, Shuwei Shi, Weihao Xia, Mingdeng Cao, Jiahao Wang , et al. (25 additional authors not shown)

Abstract: This paper reports on the NTIRE 2021 challenge on perceptual image quality assessment (IQA), held in conjunction with the New Trends in Image Restoration and Enhancement workshop (NTIRE) workshop at CVPR 2021. As a new type of image processing technology, perceptual image processing algorithms based on Generative Adversarial Networks (GAN) have produced images with more realistic textures. These o… ▽ More This paper reports on the NTIRE 2021 challenge on perceptual image quality assessment (IQA), held in conjunction with the New Trends in Image Restoration and Enhancement workshop (NTIRE) workshop at CVPR 2021. As a new type of image processing technology, perceptual image processing algorithms based on Generative Adversarial Networks (GAN) have produced images with more realistic textures. These output images have completely different characteristics from traditional distortions, thus pose a new challenge for IQA methods to evaluate their visual quality. In comparison with previous IQA challenges, the training and testing datasets in this challenge include the outputs of perceptual image processing algorithms and the corresponding subjective scores. Thus they can be used to develop and evaluate IQA methods on GAN-based distortions. The challenge has 270 registered participants in total. In the final testing stage, 13 participating teams submitted their models and fact sheets. Almost all of them have achieved much better results than existing IQA methods, while the winning method can demonstrate state-of-the-art performance. △ Less

Submitted 28 June, 2021; v1 submitted 7 May, 2021; originally announced May 2021.

Deep Hashing with Hash-Consistent Large Margin Proxy Embeddings

Authors: Pedro Morgado, Yunsheng Li, Jose Costa Pereira, Mohammad Saberian, Nuno Vasconcelos

Abstract: Image hash codes are produced by binarizing the embeddings of convolutional neural networks (CNN) trained for either classification or retrieval. While proxy embeddings achieve good performance on both tasks, they are non-trivial to binarize, due to a rotational ambiguity that encourages non-binary embeddings. The use of a fixed set of proxies (weights of the CNN classification layer) is proposed… ▽ More Image hash codes are produced by binarizing the embeddings of convolutional neural networks (CNN) trained for either classification or retrieval. While proxy embeddings achieve good performance on both tasks, they are non-trivial to binarize, due to a rotational ambiguity that encourages non-binary embeddings. The use of a fixed set of proxies (weights of the CNN classification layer) is proposed to eliminate this ambiguity, and a procedure to design proxy sets that are nearly optimal for both classification and hashing is introduced. The resulting hash-consistent large margin (HCLM) proxies are shown to encourage saturation of hashing units, thus guaranteeing a small binarization error, while producing highly discriminative hash-codes. A semantic extension (sHCLM), aimed to improve hashing performance in a transfer scenario, is also proposed. Extensive experiments show that sHCLM embeddings achieve significant improvements over state-of-the-art hashing procedures on several small and large datasets, both within and beyond the set of training classes. △ Less

Submitted 27 July, 2020; originally announced July 2020.

Comments: Accepted at International Journal of Computer Vision

Java Implementation of a Parameter-less Evolutionary Portfolio

Authors: José C. Pereira, Fernando G. Lobo

Abstract: The Java implementation of a portfolio of parameter-less evolutionary algorithms is presented. The Parameter-less Evolutionary Portfolio implements a heuristic that performs adaptive selection of parameter-less evolutionary algorithms in accordance with performance criteria that are measured during running time. At present time, the portfolio includes three parameter-less evolutionary algorithms:… ▽ More The Java implementation of a portfolio of parameter-less evolutionary algorithms is presented. The Parameter-less Evolutionary Portfolio implements a heuristic that performs adaptive selection of parameter-less evolutionary algorithms in accordance with performance criteria that are measured during running time. At present time, the portfolio includes three parameter-less evolutionary algorithms: Parameter-less Univariate Marginal Distribution Algorithm, Parameter-less Extended Compact Genetic Algorithm, and Parameter-less Hierarchical Bayesian Optimization Algorithm. Initial experiments showed that the parameter-less portfolio can solve various classes of problems without the need for any prior parameter setting technique and with an increase in computational effort that can be considered acceptable. △ Less

Submitted 26 June, 2015; originally announced June 2015.

Comments: 7 pages. arXiv admin note: substantial text overlap with arXiv:1506.08694, arXiv:1506.07980

ACM Class: I.2.8

A Java Implementation of Parameter-less Evolutionary Algorithms

Authors: José C. Pereira, Fernando G. Lobo

Abstract: The Parameter-less Genetic Algorithm was first presented by Harik and Lobo in 1999 as an alternative to the usual trial-and-error method of finding, for each given problem, an acceptable set-up of the parameter values of the genetic algorithm. Since then, the same strategy has been successfully applied to create parameter-less versions of other population-based search algorithms such as the Extend… ▽ More The Parameter-less Genetic Algorithm was first presented by Harik and Lobo in 1999 as an alternative to the usual trial-and-error method of finding, for each given problem, an acceptable set-up of the parameter values of the genetic algorithm. Since then, the same strategy has been successfully applied to create parameter-less versions of other population-based search algorithms such as the Extended Compact Genetic Algorithm and the Hierarchical Bayesian Optimization Algorithm. This report describes a Java implementation, Parameter-less Evolutionary Algorithm (P-EAJava), that integrates several parameter-less evolutionary algorithms into a single platform. Along with a brief description of P-EAJava, we also provide detailed instructions on how to use it, how to implement new problems, and how to generate new parameter-less versions of evolutionary algorithms. At present time, P-EAJava already includes parameter-less versions of the Simple Genetic Algorithm, the Extended Compact Genetic Algorithm, the Univariate Marginal Distribution Algorithm, and the Hierarchical Bayesian Optimization Algorithm. The source and binary files of the Java implementation of P-EAJava are available for free download at https://github.com/JoseCPereira/2015ParameterlessEvolutionaryAlgorithmsJava. △ Less

Submitted 26 June, 2015; originally announced June 2015.

Comments: 12 pages. arXiv admin note: text overlap with arXiv:1506.07980

ACM Class: I.2.8

A Java Implementation of the SGA, UMDA, ECGA, and HBOA

Authors: José C. Pereira, Fernando G. Lobo

Abstract: The Simple Genetic Algorithm, the Univariate Marginal Distribution Algorithm, the Extended Compact Genetic Algorithm, and the Hierarchical Bayesian Optimization Algorithm are all well known Evolutionary Algorithms. In this report we present a Java implementation of these four algorithms with detailed instructions on how to use each of them to solve a given set of optimization problems. Additiona… ▽ More The Simple Genetic Algorithm, the Univariate Marginal Distribution Algorithm, the Extended Compact Genetic Algorithm, and the Hierarchical Bayesian Optimization Algorithm are all well known Evolutionary Algorithms. In this report we present a Java implementation of these four algorithms with detailed instructions on how to use each of them to solve a given set of optimization problems. Additionally, it is explained how to implement and integrate new problems within the provided set. The source and binary files of the Java implementations are available for free download at https://github.com/JoseCPereira/2015EvolutionaryAlgorithmsJava. △ Less

Submitted 26 June, 2015; originally announced June 2015.

Comments: 6 pages

ACM Class: I.2.8

An Optimized Divide-and-Conquer Algorithm for the Closest-Pair Problem in the Planar Case

Authors: José C. Pereira, Fernando G. Lobo

Abstract: We present an engineered version of the divide-and-conquer algorithm for finding the closest pair of points, within a given set of points in the XY-plane. For this version of the algorithm we show that only two pairwise comparisons are required in the combine step, for each point that lies in the 2 delta-wide vertical slab. The correctness of the algorithm is shown for all Minkowski distances with… ▽ More We present an engineered version of the divide-and-conquer algorithm for finding the closest pair of points, within a given set of points in the XY-plane. For this version of the algorithm we show that only two pairwise comparisons are required in the combine step, for each point that lies in the 2 delta-wide vertical slab. The correctness of the algorithm is shown for all Minkowski distances with p>=1. We also show empirically that, although the time complexity of the algorithm is still O(n lg n), the reduction in the total number of comparisons leads to a significant reduction in the total execution time, for inputs with size sufficiently large. △ Less

Submitted 7 February, 2013; v1 submitted 28 October, 2010; originally announced October 2010.

Comments: This is a more complete version (14 pages) of the paper already published in the Journal of Computer Science and Technology (see Journal Reference)

ACM Class: F.2

Journal ref: Journal of Computer Science and Technology, 2012,27(4): 891-986