Recent Publications

Ramos MVM, de Queiroz RJGB, Moreira N, Almeida JB.  2016.  On the Formalization of Some Results of Context-Free Language Theory. Logic, Language, Information, and Computation – 23rd International Workshop, WoLLIC 2016. 9803 Abstract16wollic.pdf

This work describes a formalization effort, using the Coq proof assistant, of fundamental results related to the classical theory of context-free grammars and languages. These include closure properties (union, concatenation and Kleene star), grammar simplification (elimi- nation of useless symbols, inaccessible symbols, empty rules and unit rules), the existence of a Chomsky Normal Form for context-free grammars and the Pumping Lemma for context-free languages. The result is an important set of libraries covering the main results of context-free language theory, with more than 500 lemmas and theorems fully proved and checked. This is probably the most comprehensive formalization of the classical context-free language theory in the Coq proof assistant done to the present date, and includes the important result that is the formalization of the Pumping Lemma for context-free languages.

Cledou MG, Barbosa LS.  2016.  An Ontology for Licensing Public Transport Services. Proceedings of the 9th International Conference on Theory and Practice of Electronic Governance. :230–239. Abstractan_ontology_for_licensing_public_transport_services.pdf

By 2050 it is expected that 66% of the world population will reside in cities, compared to 54% in 2014. One particular challenge associated to urban population growth refers to transportation systems, and as an approach to face it, governments are investing significant efforts enhancing public transport services. An important aspect of public transport is ensuring that licensing of such services fulfill existing government regulations. Due to the differences in government regulations, and to the difficulties in ensuring the fulfillment of their specific features, many local governments develop tailored Information and Communication Technology (ICT) solutions to automate the licensing of public transport services. In this paper we propose an ontology for licensing such services following the REFSENO methodology. In particular, the ontology captures common concepts involved in the application and processing stage of licensing public bus passenger services. The main contribution of the proposed ontology is to define a common vocabulary to share knowledge between domain experts and software engineers, and to support the definition of a software product line for families of public transport licensing services.

Gonçalves RC, Pereira JO, Jimenez-Peris R.  2016.  An RDMA Middleware for Asynchronous Multi-stage Shuffling in Analytical Processing. DAIS '16: Proceedings of the 16th IFIP International Conference on Distributed Applications and Interoperable Systems. Abstract

A key component in large scale distributed analytical processing is shuffling, the distribution of data to multiple nodes such that the computation can be done in parallel. In this paper we describe the design and implementation of a communication middleware to support data shuffling for executing multi-stage analytical processing operations in parallel. The middleware relies on RDMA (Remote Direct Memory Access) to provide basic operations to asynchronously exchange data among multiple machines. Experimental results show that the RDMA-based middleware developed can provide a 75 % reduction of the costs of communication operations on parallel analytical processing tasks, when compared with a sockets middleware.

Cruz F, Maia F, Matos M, Oliveira R, Paulo J, Pereira JO, Vilaça R.  2016.  Resource Usage Prediction in Distributed Key-Value Datastores. Distributed Applications and Interoperable Systems: 16th IFIP WG 6.1 International Conference, DAIS 2016, Held as Part of the 11th International Federated Conference on Distributed Computing Techniques, DisCoTec 2016, Heraklion, Crete, Greece, June 6-9, 2. :144–159. Abstract

n/a

Rani S, Koshley DK, Halder R.  2016.  A Watermarking Framework for Outsourced and Distributed Relational Databases. In Proceedings of the 3rd International Conference on Future Data and Security Engineering (FDSE 2016). Springer LNCS 10018 Abstract19.pdf

Unlike centralized databases, watermarking of distributed databases faces serious challenges for various reasons, e.g. (i) Distribution of data (ii) Existence of replication (iii) Preservation of watermarks while partitioning and distributing databases, etc. In this paper, we propose a novel watermarking technique for distributed relational databases considering a generic scenario that supports database outsourcing and hybrid partitioning. Our approach addresses the above challenges in an effective way by maintaining metadata and by making the detection phase partition independent. To the best of our knowledge, this is the first proposal on watermarking of distributed relational databases that supports database outsourcing and its partitioning and distribution in a distributed setting.

Jana A, Halder R.  2016.  Defining Abstract Semantics for Static Dependence Analysis of Relational Database Applications. In Proceedings of the 12th International Conference on Information Systems Security (ICISS 2016). Springer LNCS Abstract18.pdf

Dependence Graph provides the basis for powerful programming tools to address a large number of software engineering activities including security analysis. This paper proposes a semantics-based static dependence analysis framework for relational database applications based on the Abstract Interpretation theory. As database attributes di ffer from traditional imperative language variables, we define abstract semantics of database applications in relational abstract domain. This allows to identify statically various parts of database information (in abstract form) possibly used or defined by database statements, leading to a more precise dependence analysis. This way the semantics-based dependence computation improves w.r.t. its syntax-based counterpart. We prove the soundness of our proposed approach which guarantees that non-overlapping of the defined-part by one statement and the used-part by another statement in abstract domain always indicates a non-dependency in practice. Furthermore the abstract semantics as a basis of the proposed framework makes it more powerful to solve undecidable scenario when initial database state is completely unknown.

Shoker A.  2016.  Exploiting Universal Redundancy. The 15th IEEE International Symposium on Network Computing and Applications. Abstractartira.pdf

Fault tolerance is essential for building reliable services; however, it comes at the price of redundancy, mainly the “replication factor” and “diversity”. With the increasing reliance on Internet-based services, more machines (mainly servers) are needed to scale out, multiplied with the extra expense of replication. This paper revisits the very fundamentals of fault tolerance and presents “artificial redundancy”: a formal generalization of “exact copy” redundancy in which new sources of redundancy are exploited to build fault tolerant systems. On this concept, we show how to build “artificial replication” and design “artificial fault tolerance” (AFT). We discuss the properties of these new techniques showing that AFT extends current fault tolerant approaches to use other forms of redundancy aiming at reduced cost and high diversity.

Santos A, Cunha A, Macedo N, Lourenço CB.  2016.  A Framework for Quality Assessment of ROS Repositories. Abstractros_quality.pdf

Robots are being increasingly used in safety-critical contexts, such as transportation and health. The need for flexible behavior in these contexts, due to human interaction factors or unstructured operating environments, led to a transition from hardware- to software-based safety mechanisms in robotic systems, whose reliability and quality is imperative to guarantee. Source code static analysis is a key component in formal software verification. It consists on inspecting code, often using automated tools, to determine a set of relevant properties that are known to influence the occurrence of defects in the final product. This paper presents HAROS, a generic, plug-in-driven, framework to evaluate code quality, through static analysis, in the context of the Robot Operating System (ROS), one of the most widely used robotic middleware. This tool (equipped with plug-ins for computing metrics and conformance to coding standards) was applied to several publicly available ROS repositories, whose results are also reported in the paper, thus providing a first overview of the internal quality of the software being developed in this community.

Fayollas C, Martinie C, Palanque P, Masci P, Harrison MD, Campos JC, Silva SR.  2016.  Evaluation of formal IDEs for human-machine interface design and analysis: the case of CIRCUS and PVSio-web. Workshop on Integrated Formal Development Environment (F-IDE 2016), co-located with FM2016. f-ide2016-camera-ready.pdf
Costa CM, Leite CRM, Sousa AL.  2016.  Efficient SQL adaptive query processing in cloud databases systems. 2016 {IEEE} Conference on Evolving and Adaptive Intelligent Systems, {EAIS} 2016, Natal, Brazil, May 23-25, 2016. :114–121. Abstract16.pdf

n/a

Oliveira B, Belo O, Macedo N.  2016.  Towards a Formal Validation of ETL Patterns Behavior. 6th International Conference on Model and Data Engineering (MEDI 2016).
Macedo N, Brunel J, Chemouil D, Cunha A, Kuperberg D.  2016.  Lightweight Specification and Analysis of Dynamic Systems with Rich Configurations. 24th ACM SIGSOFT International Symposium on the Foundations of Software Engineering (FSE 2016). 14.pdf
Almeida JB, Barbosa M, Barthe G, Dupressoir F.  2016.  Verifiable side-channel security of cryptographic implementations: constant-time MEE-CBC. Fast Software Encryption – 23nd International Workshop, FSE 2016. 9783:163–184. Abstract16fse.pdf

We provide further evidence that implementing software countermeasures against timing attacks is a non-trivial task and requires domain-specific software development processes: we report an implementation bug in the s2n library, recently released by AWS Labs. This bug (now fixed) allowed bypassing the balancing countermeasures against timing attacks deployed in the implementation of the MAC-then- Encode-then-CBC-Encrypt (MEE-CBC) component, creating a timing side-channel similar to that exploited by Lucky 13.

Although such an attack could only be launched when the MEE-CBC component is used in isolation – Albrecht and Paterson recently confirmed in independent work that s2n’s second line of defence, once reinforced, provides adequate mitigation against current adversary capabilities – its existence serves as further evidence to the fact that conventional software validation processes are not effective in the study and validation of security properties. To solve this problem, we define a methodology for proving security of implementations in the presence of timing attackers: first, prove black-box security of an algorithmic description of a cryptographic construction; then, establish functional correctness of an implementation with respect to the algorithmic description; and finally, prove that the implementation is leakage secure.

We present a proof-of-concept application of our methodology to MEE-CBC, bringing together three different formal verification tools to produce an assembly implementation of this construction that is verifiably secure against adversaries with access to some timing leakage. Our methodology subsumes previous work connecting provable security and side-channel analysis at the implementation level, and supports the verification of a much larger case study. Our case study itself provides the first provable security validation of complex timing countermeasures deployed, for example, in OpenSSL.

Almeida JB, Barbosa M, Barthe G, Dupressoir F, Emmi M.  2016.  Verifying Constant-Time Implementations. 25th USENIX Security Symposium, USENIX Security' 16. :53–70. Abstract16usenix.pdf

The constant-time programming discipline is an effective countermeasure against timing attacks, which can lead to complete breaks of otherwise secure systems. However, adhering to constant-time programming is hard on its own, and extremely hard under additional efficiency and legacy constraints. This makes automated verification of constant-time code an essential component for building secure software.

We propose a novel approach for verifying constant-time security of real-world code. Our approach is able to validate implementations that locally and intentionally violate the constant-time policy, when such violations are benign and leak no more information than the public outputs of the computation. Such implementations, which are used in cryptographic libraries to obtain important speedups or to comply with legacy APIs, would be declared insecure by all prior solutions.

We implement our approach in a publicly available, cross-platform, and fully automated prototype, ct-verif, that leverages the SMACK and Boogie tools and verifies optimized LLVM implementations. We present verification results obtained over a wide range of constant-time components from the NaCl, OpenSSL, FourQ and other off-the-shelf libraries. The diversity and scale of our examples, as well as the fact that we deal with top-level APIs rather than being limited to low-level leaf functions, distinguishes ct-verif from prior tools.

Our approach is based on a simple reduction of constant-time security of a program P to safety of a product program Q that simulates two executions of P. We formalize and verify the reduction for a core high-level language using the Coq proof assistant.