Carlos M. Luna

Fernanda Molina, Gustavo Betarte, Carlos Luna

Blockchain is an incipient technology that offers many strengths compared to traditional systems, such as decentralization, transparency and traceability. However, if the technology is to be used for processing personal data, complementary mechanisms must be identified that provide support for building systems that meet security and data protection requirements. We study the integration of off-chain capabilities in blockchain-based solutions moving data or computational operations outside the core blockchain network. We develop a thorough analysis of the European data protection regulation and discuss the weaknesses and strengths, regarding the security and privacy requirements established by that regulation, of solutions built using blockchain technology. We also put forward a methodological framework that helps systems designers in combining operational off-chain constructs with traditional blockchain functionalities in order to build more secure and privacy aware solutions. We illustrate the use of that framework presenting and discussing the design of a system that provides services to handle, store and validate digital academic certificates.

Gustavo Betarte, Maximiliano Cristiá, Carlos Luna et al.

MimbleWimble is a privacy-oriented cryptocurrency technology encompassing security and scalability properties that distinguish it from other protocols of the kind. In this paper we present and briefly discuss those properties and outline the basis of a model-driven verification approach to address the certification of the correctness of a particular implementation of the protocol.

Gustavo Betarte, Juan Campo, Felipe Gorostiaga et al.

Android embodies security mechanisms at both OS and application level. In this platform application security is built primarily upon a system of permissions which specify restrictions on the operations a particular process can perform. The critical role of these security mechanisms makes them a prime target for (formal) verification. We present an idealized model of a reference monitor of the novel mechanisms of Android 6 (and further), where it is possible to grant permissions at run time. Using the programming language of the proof-assistant Coq we have developed a functional implementation of the reference validation mechanism and certified its correctness with respect to the specified reference monitor. Several properties concerning the permission model of Android 6 and its security mechanisms have been formally formulated and proved. Applying the program extraction mechanism provided by Coq we have also derived a certified Haskell prototype of the reference validation mechanism.