Encontrados 50 documentos, a visualizar página 1 de 5
Formal verification of side-channel countermeasures using self-composition
Almeida, José Bacelar; Barbosa, Manuel; Pinto, Jorge Sousa; Vieira, BárbaraFormal verification of cryptographic software implementations poses significant challenges for off-the-shelf tools. This is due to the domain-specific characteristics of the code, involving aggressive optimizations and non-functional security requirements, namely the critical aspect of countermeasures against side-channel attacks. In this paper, we extend previous results supporting the practicality of self-com...
Using abstract interpretation to produce dependable aerospace control software
Silva, Rovedy Aparecida Busquim e; Arai, Nanci Naomi; Burgareli, Luciana Akemi; Oliveira, José M. Parente; Pinto, Jorge SousaIn the context of software dependability, the software veri- fication process has an important role. Formal verification of programs is an activity that can be inserted in this process to improve software reliability. This paper presents the defini- tion of an approach that employs a formal verification tech- nique based on abstract interpretation. The main goal is to apply this technique as a formal activity i...
Experimenting with predicate abstraction
Miraldo, Victor Cacciari; Frade, M. J.; Lourenço, Cláudio; Pinto, Jorge SousaPredicate abstraction is a technique employed in software model checking to produce abstract models that can be conservatively checked for property violations in reasonable time. The precision degree of different abstractions of the same program may differ based on (i) the set of predicates used; or (ii) the algorithmic technique employed to gen- erate the model. In this paper we explain how we have implemented...
SPARK-BMC : checking SPARK code for bugs
Lourenço, Cláudio; Miraldo, Victor Cacciari; Frade, M. J.; Pinto, Jorge SousaThe standard SPARK deductive verification tools, based on contracts, are not practical in early stages when the idea is only bug catching. We discuss the implementation of a bounded model checker for SPARK, focusing on specific challenges of this language. Our tool is fully automatic, complementing the existing tools for SPARK.
Assertion-based slicing and slice graphs
Barros, José Bernardo; Cruz, Daniela da; Henriques, Pedro Rangel; Pinto, Jorge SousaThis paper revisits the idea of slicing programs based on their axiomatic semantics, rather than using criteria based on control/data dependencies. We show how the forward propagation of preconditions and the backward propagation of postconditions can be combined in a new slicing algorithm that is more precise than the existing specification-based algorithms. The algorithm is based on (i) a precise test for re...
An approach to model checking Ada programs
Faria, José Miguel; Martins, J.; Pinto, Jorge SousaThis paper describes a tool-supported method for the formal verification of Ada programs. It presents ATOS, a tool that automati- cally extracts a model in SPIN from an Ada Program, together with a set of properties that state the correctness of the model. ATOS is also capable of extracting properties from user-provided annotations in Ada programs, inspired by the Spark Annotation language. The goal of ATOS is ...
Using term rewriting to solve bit-vector arithmetic problems - (Poster Presenta...
Abal, Iago; Cunha, Alcino; Hurd, Joe; Pinto, Jorge SousaAmong many theories supported by SMT solvers, the theory of finite-precision bit-vector arithmetic is one of the most useful, for both hardware and software systems verification. This theory is also particularly useful for some specific domains such as cryptography, in which algorithms are naturally expressed in terms of bit-vectors. Cryptol is an example of a domain-specific language (DSL) and toolset for cryp...
Using term rewriting to solve Bit-Vector arithmetic problems (Poster Presentation)
Abal, Iago; Cunha, Alcino; Hurd, Joe; Pinto, Jorge SousaAmong many theories supported by SMT solvers, the theory of finite-precision bit-vector arithmetic is one of the most useful, for both hardware and software systems verification. This theory is also particularly useful for some specific domains such as cryptography, in which algorithms are naturally expressed in terms of bit-vectors. Cryptol is an example of a domain-specific language (DSL) and toolset for cryp...
Formal verification of side channel countermeasures using self-composition
Almeida, José Bacelar; Barbosa, Manuel Bernardo; Pinto, Jorge Sousa; Vieira, BárbaraFormal verification of cryptographic software implementations poses significant challenges for off-the-shelf tools. This is due to the domain-specific characteristics of the code, involving aggressive optimisations and non-functional security requirements, namely the critical aspect of countermeasures against side-channel attacks. In this paper we extend previous results supporting the practicality of self-comp...
Verification conditions for source-level imperative programs
Frade, M. J.; Pinto, Jorge SousaThis paper is a systematic study of verification conditions and their use in the context of program verification. We take Hoare logic as a starting point and study in detail how a verification conditions generator can be obtained from it. The notion of program annotation is essential in this process. Weakest preconditions and the use of updates are also studied as alternative approaches to verification conditio...
| Financiadores do RCAAP | |||||||
|
|
|
|
|
|
||