Recent Publications

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.

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

n/a

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

n/a

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
n/a
Madeira A, Martins MA, Barbosa LS.  2016.  A logic for n-dimensional hierarchical refinement. Proceedings 17th International Workshop on Refinement, Refine@FM 2015, Oslo, Norway, 22nd June 2015. 209:40–56.2.pdf
Madeira A, Barbosa LS, Hennicker R, Martins MA.  2016.  Dynamic Logic with Binders and Its Application to the Development of Reactive Systems. Theoretical Aspects of Computing - ICTAC 2016 - 13th International Colloquium, Taipei, Taiwan, ROC, October 24-31, 2016, Proceedings. 9965:422–440. Abstractmbhm16.pdf

This paper introduces a logic to support the specification and development of reactive systems on various levels of abstraction, from property specifications, concerning e.g. safety and liveness requirements, to constructive specifications representing concrete processes. This is achieved by combining binders of hybrid logic with regular modalities of dynamic logics in the same formalism, which we call D↓-logic. The semantics of our logic focuses on effective processes and is therefore given in terms of reachable transition systems with initial states. The second part of the paper resorts to this logic to frame stepwise development of reactive systems within the software development methodology proposed by Sannella and Tarlecki. In particular, we instantiate the generic concepts of constructor and abstractor implementations by using standard operators on reactive components, like relabelling and parallel composition, as constructors, and bisimulation for abstraction. We also study vertical composition of implementations which relies on the preservation of bisimularity by the constructions on labeleld transition systems.

Neves R, Barbosa LS.  2016.  Hybrid Automata as Coalgebras. Theoretical Aspects of Computing - ICTAC 2016 - 13th International Colloquium, Taipei, Taiwan, ROC, October 24-31, 2016, Proceedings. 9965:385–402. Abstractnb16.pdf

Able to simultaneously encode discrete transitions and continuous behaviour, hybrid automata are the de facto framework for the formal specification and analysis of hybrid systems. The current paper revisits hybrid automata from a coalgebraic point of view. This allows to interpret them as state-based components, and provides a uniform theory to address variability in their definition, as well as the corresponding notions of behaviour, bisimulation, and observational semantics.

Fernandes S, Barbosa LS.  2016.  Applying the 3C Model to FLOSS Communities. Collaboration and Technology - 22nd International Conference, CRIWG 2016, Kanazawa, Japan, September 14-16, 2016, Proceedings. 9848:139–150. Abstractfb16a.pdf

How learning occurs within Free/Libre Open Source (FLOSS) communities and what is the dynamics such projects (e.g. the life cycle of such projects) are very relevant questions when considering the use of FLOSS projects in a formal education setting. This paper introduces an approach based on the 3C collaboration model (communication, coordination and cooperation) to represent the collaborative learning dynamics within FLOSS communities. To explore the collaborative learning potential of FLOSS communities a number of questionnaires and interviews to selected FLOSS contributors were run. From this study a 3C collaborative model applicable to FLOSS communities was designed and discussed.

Veiga L, Janowski T, Barbosa LS.  2016.  Digital Government and Administrative Burden Reduction. Proceedings of the 9th International Conference on Theory and Practice of Electronic Governance, ICEGOV 2016, Montevideo, Uruguay, March 1-3, 2016. :323–326. Abstractvjb16.pdf

Administrative burden represents the costs to businesses, citizens and the administration itself of complying with government regulations and procedures. The burden tends to increase with new forms of public governance that rely less on direct decisions and actions undertaken by traditional government bureaucracies, and more on government creating and regulating the environment for other, non-state actors to jointly address public needs. Based on the reviews of research and policy literature, this paper explores administrative burden as a policy problem, presents how Digital Government (DG) could be applied to address this problem, and identifies societal adoption, organizational readiness and other conditions under which DG can be an effective tool for Administrative Burden Reduction (ABR). Finally, the paper tracks ABR to the latest Contextualization stage in the DG evolution, and discusses possible development approaches and technological potential of pursuing ABR through DG.

Oliveira N, Barbosa LS.  2016.  An Enhanced Model for Stochastic Coordination. Proceedings of the First International Workshop on Formal Methods for and on the Cloud, iFMCloud@IFM 2016, Reykjavik, Iceland, 4th June 2016.. 228:35–45. Abstractob16.pdf

Applications developed over the cloud coordinate several, often anonymous, computational resources, distributed over different execution nodes, within flexible architectures. Coordination models able to represent quantitative data provide a powerful basis for their analysis and validation. This paper extends IMCreo, a semantic model for Stochastic reo based on interactive Markov chains, to enhance its scalability, by regarding each channel and node, as well as interface components, as independent stochastic processes that may (or may not) synchronise with the rest of the coordination circuit.