Recent Publications

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


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.

Pontes R, Maia F, Paulo J, Vilaça R.  2016.  SafeRegions: Performance Evaluation of Multi-party Protocols on HBase. 2016 IEEE 35th Symposium on Reliable Distributed Systems Workshops (SRDSW), 2016 . :31-36.13.pdf
Burihabwa D, Pontes R, Felber P, Maia F, Mercier H, Oliveira R, Paulo J, Schiavoni V.  2016.  On the Cost of Safe Storage for Public Clouds: an Experimental Evaluation.. 35th IEEE International Symposium on Reliable Distributed Systems 2016.. 12.pdf
Kolev B, Bondiombouy C, Valduriez P, Jimenez-Peris R, Pau R, Pereira JO.  2016.  The CloudMdsQL Multistore System. Proceedings of the 2016 International Conference on Management of Data. :2113–2116. Abstract11.pdf


Kolev B, Bondiombouy C, Levchenko O, Valduriez P, Jimenez-Peris R, Pau R, Pereira JO.  2016.  Design and Implementation of the CloudMdsQL Multistore System. Proceedings of the 6th International Conference on Cloud Computing and Services Science. :352-359. Abstract10.pdf


Santiago RHN, Bedregal B{\'ı}nRC, Madeira A, Martins MA.  2016.  On Interval Dynamic Logic. Formal Methods: Foundations and Applications - 19th Brazilian Symposium, {SBMF} 2016, Natal, Brazil, November 23-25, 2016, Proceedings. :129–144. Abstract