Publications

Barbosa MB, Castro D, Silva P.  2014.  Compiling CAO: From Cryptographic Specifications to C Implementations. Principles of Security and Trust. 8414:240-244. Abstractpost14.pdf

We present a compiler for CAO, an imperative DSL for the cryptographic domain. The tool takes high-level cryptographic algorithm specifications and translates them into C implementations through a series of security-aware transformations and optimizations.
The compiler back-end is highly configurable, allowing the targeting of very disparate platforms in terms of memory requirements and computing power.
Ferreira JF, Mendes A, Cunha A, Moreno CB, Silva P, Barbosa LS, Oliveira JN.  2011.  Logic Training through Algorithmic Problem Solving. Tools for Teaching Logic. 6680:62-69. Abstractticttl11.pdf

Although much of mathematics is algorithmic in nature, the skills needed to formulate and solve algorithmic problems do not form an integral part of mathematics education. In particular, logic, which is central to algorithm development, is rarely taught explicitly at pre university level, under the justi cation that it is implicit in mathematics and therefore does not need to be taught as an independent topic. This paper argues in the opposite direction, describing a one week workshop done at the University of Minho, in Portugal, whose goal was to introduce to high-school students calculational principles and techniques of algorithmic problem solving supported by calculational logic. The work shop resorted to recreational problems to convey the principles and to software tools, the Alloy Analyzer and Netlogo, to animate models.
Barbosa MB, Moss A, Page D, Rodrigues N, Silva P.  2011.  Type Checking Cryptography Implementations. Fundamentals of Software Engineering - 4th IPM International Conference, FSEN 2011, Revised Selected Papers. 7141:316-334. Abstractfsen11.pdf

Cryptographic software development is a challenging field: high performance must be achieved, while ensuring correctness and compliance with low-level security policies. CAO is a domain specific language designed to assist development of cryptographic software. An important feature of this language is the design of a novel type system introducing native types such as predefined sized vectors, matrices and bit strings, residue classes modulo an integer, finite fields and finite field extensions, allowing for extensive static validation of source code. We present the formalisation, validation and implementation of this type system.
Silva P, Visser J, Oliveira JN.  2009.  Galois: A Language for Proofs Using Galois Connections and Fork Algebras. PLMMS'09 - ACM SIGSAM 2009 International Workshop on Programming Languages for Mechanized Mathematics Systems. Abstractplmms09.pdf

Galois is a domain specific language supported by the Galculator interactive proof-assistant prototype. Galculator uses an equational approach based on Galois connections with indirect equality as an additional inference rule. Galois allows for the specification of different theories in a point-free style by using fork algebras, an extension of relation algebras with expressive power of first-order logic. The language offers sub-languages to derive proof rules from Galois connections, to express proof tactics, and to organize axioms and theorems into modular definitions.

In this paper, we describe how the algebraic theory underlying the proof-method drives the design of the Galois language. We provide the syntax and semantics of important fragments of Galois and show how they are hierarchically combined into a complete language.
Silva P, Oliveira JN.  2008.  'Galculator': functional prototype of a Galois-connection based proof assistant. Proceedings of 10th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming. :44-55. Abstractppdp08.pdf

Galculator is the name of the prototype of a proof assistant of a special brand: it is solely based on the algebra of Galois connections. When combined with the pointfree transform and tactics such as the indirect equality principle, Galois connections offer a very powerful, generic device to tackle the complexity of proofs in program verification. The paper describes the architecture of the current Galculator prototype, which is implemented in Haskell in order to steer types as much as possible. The prospect of integrating the Galculator with other proof assistants such as e.g. Coq is also discussed.
Alves T, Silva P, Visser J, Oliveira JN.  2005.  Strategic Term Rewriting and Its Application to a VDMSL to SQL Conversion. FM - Proceedings of International Symposium of Formal Methods Europe. 3582:399-414. Abstractfm05.pdf

We constructed a tool, called VooDooM, which converts datatypes in VDM-SL into SQL relational data models. The conversion involves transformation of algebraic types to maps and products, and pointer introduction.
The conversion is specified as a theory of refinement by calculation. The implementation technology is strategic term rewriting in Haskell, as supported by the Strafunski bundle. Due to these choices of theory and technology, the road from theory to practise is straightforward.
Alves T, Silva P, Visser J.  2012.  Constraint-aware Schema Transformation. Electronic Notes in Theoretical Computer Science. 290:3-18. Abstractrule08.pdf

Data schema transformations occur in the context of software evolution, refactoring, and cross-paradigm data mappings. When constraints exist on the initial schema, these need to be transformed into constraints on the target schema. Moreover, when high-level data types are refined to lower level structures, additional target schema constraints must be introduced to balance the loss of structure and preserve semantics.

We introduce an algebraic approach to schema transformation that is constraint-aware in the sense that constraints are preserved from source to target schemas and that new constraints are introduced where needed. Our approach is based on refinement theory and point-free program transformation. Data refinements are modeled as rewrite rules on types that carry point-free predicates as constraints. At each rewrite step, the predicate on the reduct is computed from the predicate on the redex. An additional rewrite system on point-free functions is used to normalize the predicates that are built up along rewrite chains.

We implemented our rewrite systems in a type-safe way in the functional programming language Haskell. We demonstrate their application to constraint-aware hierarchical-relational mappings.
Barbosa MB, Moss A, Page D, Rodrigues N, Silva P.  2011.  Type Checking Cryptography Implementations. Abstractdi-cctc-11-01.pdf

Cryptographic software development is a challenging field: high performance must be achieved, while ensuring correctness and compliance with low-level security policies. CAO is a domain specific language designed to assist development of cryptographic software. An important feature of this language is the design of a novel type system introducing native types such as predefined sized vectors, matrices and bit strings, residue classes modulo an integer, finite fields and finite field extensions, allowing for extensive static validation of source code. We present the formalisation, validation and implementation of this type system.
Silva P, Oliveira JN.  2008.  Report on the Design of a Galculator. Abstracttechicalreport-fast-08-01.pdf

This report presents the Galculator, a tool aimed at deriving equational proofs in arbitrary domains using Galois connections as the fundamental concept. When combined with the pointfree transform and the indirect equality principle, Galois connections offer a very powerful, generic device to tackle the complexity of proofs in program verification.

We show how rewriting rules derived from the properties of the Galois connections are applied in proofs using a strategic term rewriting system which, in the current prototype, is implemented in Haskell. The prospect of integrating the Galculator with other proof assistants such as e.g. Coq is also discussed.
Silva P.  2009.  On the Design of a Galculator. Abstractthesis.pdf

The increased complexity of software systems together with the lack of tools and technique to support their development led to the so-called "software crisis". Different views about the problem originated diverse approaches to a possible solution, although it is now generally accepted that a "silver bullet" does not exist.
The formal methods view considers mathematical reasoning as fundamental to fulfill the most important property of software systems: correctness. However, since correctness proofs are generally difficult and expensive, only critical applications are regarded as potential targets for their use. Developments in tool support such as proof assistants, model checkers and abstract interpreters allows for reducing this cost and making proofs affordable to a wider range of applications. Nevertheless, the effectiveness of a tool is highly dependent of the underlying theory.
This dissertation follows a calculational proof style in which equality plays the fundamental role. Instead of the traditional logical approach, fork algebras, an extension of relation algebras, are used. In this setting, Galois connections are important because they reinforce the calculational nature of the algebraic approach, bringing additional structure to the calculus. Moreover, Galois connections enjoy several valuable proper- ties and allow for transformation in the domain of problems. In this dissertation, it is shown how fork algebras and Galois connections can be integrated together with the indirect equality principle. This combination offers a very powerful, generic device to tackle the complexity of proofs in program verification. This power is enhanced with the design of an innovative proof assistant prototype, the Galculator.