Towards Secure Distributed Computations
Nowadays, there are plenty of networks that work in a cooperative way and form what we know as grids of computers. These grids are serving a lot of purposes, and they are used with good results for intensive calculation, because the joined computing power aids in solving complex functions. To cope with these new requirements and facilities, programming languages have had to evolve to new paradigms, including facilities to do distributed computing in a straightforward way.
Formal analysis of security models for mobile devices, virtualization platforms, and domain name systems
In this thesis we investigate the security of security-critical applications, i.e. applications in which a failure may produce consequences that are unacceptable. We consider three areas: mobile devices, virtualization platforms, and domain name systems.The Java Micro Edition platform denes the Mobile Information Device Prole (MIDP) to facilitate the development of applications for mobile devices, like cell phones and PDAs. In this work we first study and compare formally several variants of the security model specified by MIDP to access sensitive resources of a mobile device.Hypervisors allow multiple guest operating systems to run on shared hardware, and offer a compelling means of improving the security and the flexibility of software systems. In this thesis we present a formalization of an idealized model of a hypervisor, and we establish (formally) that the hypervisor ensures strong isolation properties between the different operating systems, and guarantees that requests from guest operating systems are eventually attended. We show also that virtualized platforms are transparent, i.e. a guest operating system cannot distinguish whether it executes alone or together with other guest operating systems on the platform.The Domain Name System Security Extensions (DNSSEC) is a suite of specifications that provides origin authentication and integrity assurance services for DNS data. We finally present a minimalistic specification of a DNSSEC model which provides the grounds needed to formally state and verify security properties concerning the chain of trust of the DNSSEC tree.We develop all our formalizations in the Calculus of Inductive Constructions –formal language that combines a higher-order logic and a richly-typed functional programming language– using the Coq proof assistant.
Formally verified countermeasures against cache based attacks in virtualization platforms
Cache based attacks are a class of side-channel attacks that are particularly effective in virtualized or cloud-based environments, where they have been used to recover secret keys from cryptographic implementations. One common approach to thwart cache-based attacks is to use constant-time implementations, which do not branch on secrets and do not perform memory accesses that depend on secrets. However, there is no rigorous proof that constant-time implementations are protected against concurrent cache attacks in virtualization platforms; moreover, many prominent implementations are not constant-time. An alternative approach is to rely on system-level mechanisms. One recent such mechanism is stealth memory, which provisions a small amount of private cache for programs to carry potentially leaking computations securely. We weaken the definition of constant-time, introducing a new program classification called S-constant-time, that captures the behavior of programs that correctly use stealth memory. This new definition encompasses some widely used cryptographic implementations. However, there was no rigorous analysis of stealth memory and S-constant-time, and no tool support for checking if applications are S-constant-time. In this thesis, we propose a new information-flow analysis that checks if an x86 application executes in constant-time or S-constant-time. Moreover, we prove that (S-)constant-time programs do not leak confidential information through the cache to other operating systems executing concurrently on virtualization platforms. The soundness proofs are based on new theorems of independent interest, including isolation theorems for virtualization platforms, and proofs that (S-)constant-time implementations are non-interfering with respect to a strict information flow policy which disallows that control flow and memory accesses depend on secrets. We formalize our results using the Coq proof assistant and we demonstrate the effectiveness of our analyses on cryptographic implementations, including PolarSSL AES, DES and RC4, SHA256 and Salsa20.
Enhancing web application attack detection using machine learning
Despite all effort of the security community, for example initiatives as the OWASP Top 10, it is a known fact that web applications are permanently being exposed to attacks that exploit their vulnerabilities. Some web applications vulnerabilities can only be discovered as a result of a process of trial and error performed by an at- tacker. The identification and determination of a user’s behavior using attack detec- tion techniques become crucial, these techniques assist in aspects such as preventing attackers to identify/verify successfully the existence of vulnerabilities in applica- tions and to minimize the number of false positives (non-malicious activity identi- fied as such). A technological alternative for performing real-time attack analysis is the use of a Web Application Firewall (WAF), systems that intercepts and inspects all traffic between the web server and its clients, searching for attacks in the communi- cation’s content. Most WAF works by using a set of statics rules defined to identify attacks.
Offloading cryptographic services to the SIM card in smartphones
Smartphones have achieved ubiquitous presence in people’s everyday life as communication, entertainment and work tools. Touch screens and a va- riety of sensors offer a rich experience and make applications increasingly diverse, complex and resource demanding. Despite their continuous evolu- tion and enhancements, mobile devices are still limited in terms of battery life, processing power, storage capacity and network bandwidth. Computa- tion offloading stands out among the efforts to extend device capabilities and face the growing gap between demand and availability of resources. As most popular technologies, mobile devices are attractive targets for malicious at- tackers. They usually store sensitive private data of their owners and are increasingly used for security sensitive activities such as online banking or mobile payments. While computation offloading introduces new challenges to the protection of those assets, it is very uncommon to take security and privacy into account as the main optimization objectives of this technique. Mobile OS security relies heavily on cryptography. Available hardware and software cryptographic providers are usually designed to resist software attacks. This kind of protection is not enough when physical control over the device is lost. Secure elements, on the other hand, include a set of protections that make them physically tamper-resistant devices. This work proposes a computation offloading technique that prioritizes enhancing security capabilities in mobile phones by offloading cryptographic operations to the SIM card, the only universally present secure element in those devices. Our contributions include an architecture for this technique, a proof-of-concept prototype developed under Android OS and the results of a performance evaluation that was conducted to study its execution times and battery consumption. Despite some limitations, our approach proves to be a valid alternative to enhance security on any smartphone.
Web Application Attacks Detection Using Deep Learning
In the thesis, we present the use of deep learning techniques to improve the performance of Web Application Firewalls (WAFs), systems that are used to detect and prevent attacks to web applications. Typically a WAF inspects the HyperText Transfer Protocol (HTTP) requests that are exchanged between client and server to spot attacks and block potential threats. We model the problem as a one-class supervised case and build a feature extractor using a deep learning technique. We treat the HTTP requests as text and train a deep language model with a transformer encoder architecture which is a self- attention-based neural network. The use of pre-trained language models has yielded significant improvements on a diverse set of NLP tasks because they are capable of doing transfer learning. We use the pre-trained model as a feature extractor to map the HTTP requests into feature vectors. Then, these vectors are used to train a one-class classifier. We also use an established performance metric to define an operational point for the one-class model automatically. The experimental results show that the proposed approach outperforms the ones of the classic rule-based ModSecurity configured with a vanilla CRS and does not require the participation of a security expert to define the features.
Constructing privacy aware blockchain solutions: Design guidelines and threat analysis techniques
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. In this work we study the integration of off-chain capabilities in blockchain-based solutions, moving data or computational operations outside the core blockchain network. Additionally, we develop a thorough analysis of the European and Uruguayan 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. Based on this analysis, we present a system architecture for the design of privacy aware solutions that are built using blockchain technology. We also put forward a systematic approach for performing a security and privacy threat analysis of such kind of solutions. Finally, we illustrate the use of the proposed methodological tools, presenting and discussing both the design and the security and privacy assessment of a system that provides services to handle, store and validate digital academic certificates.
A Formal Analysis of the Mimblewimble Cryptocurrency Protocol with a Security Approach
A cryptocurrency is a digital currency that can be exchanged online for goods and services. Cryptocurrencies are deployed over public blockchains which have the transactions duplicated and distributed across the nodes of a computer network. This decentralized mechanism is devised in order to achieve reliability in a network consisting of unreliable nodes. Privacy, anonymity and security have become crucial in this context. For that reason, formal and mathematical approaches are gaining popularity in order to guarantee the correctness of the cryptocurrency implementations. Mimblewimble is a privacy-oriented cryptocurrency technology which provides security and scalability properties that distinguish it from other protocols of its kind. It was proposed by an anonymous developer, who posted a link to a text file on the IRC channel by the name Tom Elvis Jedusor (french name for Voldemort in Harry Potter) in mid-2016. Mimblewimble’s cryptographic approach is based on Elliptic Curve Cryptography which allows to verify a transaction without revealing any information about the transactional amount or the parties involved. Mimblewimble combines Confidential transactions, CoinJoin and cut-through to achieve a higher level of privacy and security, as well as, scalability. In this thesis, we present and discuss these security properties and outline the basis of a model-driven verification approach to address the certification of the correctness of the protocol implementations. In particular, we propose an idealized model that is key in the described verification process. The main components of our idealized model are transactions, blocks and chain. Then, we identify and precisely state the conditions for our model to ensure the verification of relevant security properties of Mimblewimble. In addition, we analyze the Grin and Beam implementations of Mimblewimble in their current state of development. We present detailed connections between our model and their implementations regarding the Mimblewimble structure and its security properties.
Detection and classification of privacy leaks enabled by third-party trackers in COVID-19 mobile applications
Since 2019, the world has been experiencing a pandemic without precedents in our current technological era. Governments and other high-profile organizations devoted special efforts to developing and sponsoring mobile applications that, while varying in their goals, tried to help contain the spread of COVID-19 and enable people to have the best quality of life possible. However, while third-party libraries and their impact on the user’s privacy have been studied before, especially those considered trackers, these have found their way into COVID-19 applications backed by high-profile orga- nizations. By trackers we considered third-party libraries included in applications to provide certain functionalities that, in addition, gather information regarding the ap- plication, the device and their use, and send it to their servers. The research for this thesis found that 402 out of 595 studied applications contained at least one tracker. In addition, it was confirmed that sensitive information was transferred to the tracker servers, potentially disclosing the health status of the application users. On the other hand, evidence indicates that governments can improve their data protection impact assessments and the disclosure they make in their privacy policies; the latter also ap- plies to trackers. Finally, SAPITO, an easy-to-use open-source tool, is presented. Based on the knowledge and lessons learned during this research, it was created with the ob- jective of helping privacy teams and researchers to detect automatically data leakages when analyzing third-party libraries in Android applications.