Search

MicroScope and other similar microarchitectural replay attacks take advantage of the characteristics of speculative execution to trap the execution of the victim application in a loop, enabling the attacker to amplify a side-channel attack by executing it indefinitely. Due to the nature of the replay, it can be used to effectively attack software that are shielded against replay, even under conditions where a side-channel attack would not be possible (e.g., in secure enclaves). At the same time, unlike speculative side-channel attacks, microarchitectural replay attacks can be used to amplify the correct path of execution, rendering many existing speculative side-channel defenses ineffective. In this work, we generalize microarchitectural replay attacks beyond MicroScope and present an efficient defense against them. We make the observation that such attacks rely on repeated squashes of so-called “replay handles” and that the instructions causing the side-channel must reside in the same reorder buffer window as the handles. We propose Delay-on-Squash, a hardware-only technique for tracking squashed instructions and preventing them from being replayed by speculative replay handles. Our evaluation shows that it is possible to achieve full security against microarchitectural replay attacks with very modest hardware requirements while still maintaining 97% of the insecure baseline performance.

Cyberattacks are the fastest growing crime in the U.S., and they are increasing in size, sophistication, and cost. These attacks use vulnerabilities to compromise systems to leak Information (Yahoo 2016, Marriott 2018, and Facebook 2019), steal identity information (Equifax 2017), or even effecting politics (by attacking the governmental election process). Traditionally, security researchers and practitioners have viewed security as a software problem -- originating in software and to be solved by software. Recently, the Spectre and Meltdown attacks have shown that hardware should also be considered when evaluating the system security. Conversely, because many aspects of security are computationally expensive, hardware can play a role in promoting software security through computational support as well as the development of new abstractions that promote security. Under this general umbrella, the research in this dissertation pursues two research directions that demonstrate how hardware can promote software security, and how we can design hardware that is secure against Spectre and Meltdown attacks. In the first direction, security exploits and ensuant malware pose an increasing challenge to computing systems as the variety and complexity of attacks continue to increase. In response, software-based malware detection tools have grown in complexity, thus making it computationally difficult to use them to protect systems in real-time. Against this drawback, hardware-based malware detectors (HMDs) are a promising new approach to defend against malware. HMDs collect low-level architectural features and use them to classify malware from normal programs. With simple hardware support, HMDs can be always on, operating as a first line of defense that prioritizes the application of more expensive and more accurate software-detector. In this dissertation, our goal is to make HMDs practical for deployment in two ways: (1) Improving the detection accuracy of HMDs: We use specialized detectors targeted towards a specific type of malware to improve the detection of each type. Next, we use ensemble learning techniques to improve the overall accuracy by combining detectors. We explore detectors based on logistic regression (LR) and neural networks (NN). The proposed detectors reduce the false-positive rate by more than half compared to using a single detector, while increasing their sensitivity. We develop metrics to estimate detection overhead; the proposed detectors achieve more than 16.6x overhead reduction during online detection compared to an idealized software-only detector, with an 8x improvement in relative detection time. NN detectors outperform LR detectors in accuracy, overhead (by 40\%), and time-to-detection of the hardware component (by 5x). Finally, we characterize the hardware complexity by extending an open-core and synthesizing it on an FPGA platform, showing that the overhead is minimal. (2) Make them resilient to evasion attacks: we explore the question of how well evasive malware can avoid detection by HMDs. We show that existing HMDs can be effectively reverse-engineered and subsequently evaded, allowing malware to hide from detection without substantially slowing it down (which is important for certain types of malware). This result demonstrates that the current generation of HMDs can be easily defeated by evasive malware. Next, we explore how well a detector can evolve if it is exposed to this evasive malware during training. We show that simple detectors, such as logistic regression, cannot detect the evasive malware even with retraining. More sophisticated detectors can be retrained to detect evasive malware, but the retrained detectors can be reverse-engineered and evaded again. To address these limitations, we propose a new type of Resilient HMDs (RHMDs) that stochastically switch between different detectors. These detectors can be shown to be provably more difficult to reverse engineer based on resent results in probably approximately correct (PAC) learnability theory. We show that indeed such detectors are resilient to both reverse engineering and evasion, and that the resilience increases with the number and diversity of the individual detectors. Our results demonstrate that these HMDs offer effective defense against evasive malware at low additional complexity. In the second direction, the recent Spectre and Meltdown attacks show that speculative execution, which is used pervasively in modern CPUs, can leave side effects in the processor caches and other structures even when the speculated instructions do not commit and their direct effect is not visible. Therefore, they utilize this behavior to expose privileged information accessed speculatively to an unprivileged attacker. In particular, the attack forces the speculative execution of a code gadget that will carry out the illegal read, which eventually gets squashed, but which leaves a side-channel trail that can be used by the attacker to infer the value. Several attack variations are possible, allowing arbitrary exposure of the full kernel memory to an unprivileged attacker. In this dissertation, we introduce a new model (SafeSpec) for supporting speculation in a way that is immune to the side- channel leakage necessary for attacks such as Meltdown and Spectre. In particular, SafeSpec stores side effects of speculation in separate structures while the instructions are speculative. The speculative state is then either committed to the main CPU structures if the branch commits, or squashed if it does not, making all direct side effects of speculative code invisible. The solution must also address the possibility of a covert channel from speculative instructions to committed instructions before these instructions are committed (i.e., while they share the speculative state). We show that SafeSpec prevents all three variants of Spectre and Meltdown, as well as new variants that we introduce. We also develop a cycle accurate model of modified design of an x86-64 processor and show that the performance impact is negligible (in fact a small performance improvement is achieved). We build prototypes of the hardware support in a hardware description language to show that the additional overhead is acceptable. SafeSpec completely closes this class of attacks, retaining the benefits of speculation, and is practical to implement.

Recent advances in machine learning have enabled Neural Network (NN) inference directly on constrained embedded devices. This local approach enhances the privacy of user data, as the inputs to the NN inference are not shared with third-party cloud providers over a communication network. At the same time, however, performing local NN inference on embedded devices opens up the possibility of Power Analysis attacks, which have recently been shown to be effective in recovering NN parameters, as well as their activations and structure. Knowledge of these NN characteristics constitutes a privacy threat, as it enables highly effective Membership Inference and Model Inversion attacks, which can recover information about the sensitive data that the NN model was trained on. In this paper we address the problem of securing sensitive NN inference parameters against Power Analysis attacks. Our approach employs masking, a countermeasure well-studied in the context of cryptographic algorithms. We design a set of gadgets, i.e., masked operations, tailored to NN inference. We prove our proposed gadgets secure against power attacks and show, both formally and experimentally, that they are composable, resulting in secure NN inference. We further propose optimizations that exploit intrinsic characteristics of NN inference to reduce the masking’s runtime and randomness requirements. We empirically evaluate the performance of our constructions, showing them to incur a slowdown by a factor of about 2–5.

Secure compilation is an emerging field that puts together advances in security, programming languages, compilers, verification, systems, and hardware architectures in order to devise more secure compilation chains that eliminate many of today’s security vulnerabilities and that allow sound reasoning about security properties in the source language. For a concrete example, all modern languages provide a notion of structured control flow and an invoked procedure is expected to return to the right place. However, today’s compilation chains (compilers, linkers, loaders, runtime systems, hardware) cannot efficiently enforce this abstraction against linked low-level code, which can call and return to arbitrary instructions or smash the stack, blatantly violating the high-level abstraction. Other problems arise because today’s languages fail to specify security policies, such as data confidentiality, and the compilation chains thus fail to enforce them, especially against powerful side-channel attacks. The emerging secure compilation community aims to address such problems by identifying precise security goals and attacker models, designing more secure languages, devising efficient enforcement and mitigation mechanisms, and developing effective verification techniques for secure compilation chains. This seminar strived to take a broad and inclusive view of secure compilation and to provide a forum for discussion on the topic. The goal was to identify interesting research directions and open challenges by bringing together people working on building secure compilation chains, on designing security enforcement and attack-mitigation mechanisms in both software and hardware, and on developing formal verification techniques for secure compilation., DagRep, Volume 11, Issue 10, pages 173-204

Our society is increasingly dependent on computer systems. Ensuring their security is essential to avoid the dramatic consequences of attacks against these systems. In this thesis, we focus on a class of attacks called timing sidechannel attacks. We study existing protections against these attacks, such as the constant-time and the constant-resource policies, and focus on their interaction with compilation. Compilation is the process of transforming a program written by a human in a source language, into machine code executable by a computer. Our goal is to ensure that compilation does not introduce any vulnerability in the compiled code, with respect to the security policies we focus on; this is called secure compilation. Our work also relies on formal methods to give formal guarantees on the results we present. One of our contribution relies on the formally verified CompCert compiler. All the results presented in this thesis are mechanically verified using the Coq proof assistant.; Notre société est de plus en plus dépendante des systèmes informatiques. Assurer leur sécurité est essentiel pour éviter les conséquences dramatiques des attaques contre ces systèmes. Dans cette thèse, nous nous concentrons sur une classe d’attaques appelée attaques par canaux cachés temporels. Nous étudions les protections existantes contre ces attaques, telles que les politiques constant-time et constant-resource, et nous nous concentrons sur leur interaction avec la compilation. La compilation est le processus de transformation d’un programme écrit par un humain dans un langage source, en code machine exécutable par un ordinateur. Notre objectif est de s’assurer que la compilation n’introduit aucune vulnérabilité dans le code compilé, par rapport aux politiques de sécurité auxquelles nous nous intéressons ; c’est ce qu’on appelle la compilation sécurisée. Notre travail s’appuie également sur des méthodes formelles pour donner des garanties formelles sur les résultats que nous présentons. Une de nos contributions s’appuie sur le compilateur formellement vérifié CompCert. Tous les résultats présentés dans cette thèse sont également vérifiés mécaniquement en utilisant l’assistant de preuve Coq.

We present Xenon, a solver-aided, interactive method for formally verifying that Verilog hardware executes in constant-time. Xenon scales to realistic hardware designs by drastically reducing the effort needed to localize the root cause of verification failures via a new notion of constant-time counterexamples, which Xenon uses to synthesize a minimal set of secrecy assumptions in an interactive verification loop. To reduce verification time Xenon exploits modularity in Verilog code via module summaries, thereby avoiding duplicate work across multiple module instantiations. We show how Xenon's assumption synthesis and summaries enable us to verify different kinds of circuits, including a highly modular AES- 256 implementation where modularity cuts verification from six hours to under three seconds, and the ScarVside-channel hardened RISC-V micro-controller whose size exceeds previously verified designs by an order of magnitude. In a small study, we also find that Xenon helps non-expert users complete verification tasks correctly and faster than previous state-of-art tools.

In this research, we explore the alluviation process of an artificial side-channel built in August 2015 and designed to alleviate bank erosion risks on the main river. The study area is located on the lower Gállego River, a meandering-wandering gravel-bed river draining the Southern Pyrenees. This river reach is still dynamic (i.e. chutes, meander migration and other riverine processes are often observed during floods) despite the presence of three dams in the upper catchment, encroachments and extensive mining during the 1960s–80s that led to severe incision. In this research, we focus on the effects of bankfull-like flood events (Qpeak¿=¿354¿m3/s) between February 2016 and February 2017, which alluviated 62% of the side-channel. This research aims at finding the physical mechanisms that explain the alluviation process and at putting them in the general context of the current geomorphic trend of the Gállego River in response to past and ongoing impacts. The causes of the alluviation are studied through collecting and analysing field data, which in turn, are used as input in a novel modelling strategy that includes one-dimensional hydraulic modelling, semi-empirical expressions to obtain the sediment supply entering the side-channel system and a morphodynamic model able to deal with granular sediment mixtures in compound channels. The analyses of the numerical results along with the recent history of impacts and general channel pattern adjustments help us understand about the morphodynamics mechanisms responsible for the alluviation of the side-channel.

Bluetooth Low Energy (BLE) devices use public (non-encrypted) advertising channels to announce their presence to other devices. To prevent tracking on these public channels, devices may use a periodically changing, randomized address instead of their permanent Media Access Control (MAC) address. In this work we show that many state-of-the-art devices which are implementing such anonymization measures are vulnerable to passive tracking that extends well beyond their address randomization cycles. We show that it is possible to extract identifying tokens from the pay-load of advertising messages for tracking purposes. We present an address-carryover algorithm which exploits the asynchronous nature of payload and address changes to achieve tracking beyond the address randomization of a device. We furthermore identify an identity-exposing attack via a device accessory that allows permanent, non-continuous tracking, as well as an iOS side-channel which allows insights into user activity. Finally, we provide countermeasures against the presented algorithm and other privacy flaws in BLE advertising.

Today, with the advent of IoT and the resulting fragmentation of wireless technologies, they bring not only benefits, but also concerns. Daily, several individuals communicate with each other using various communication methods. Individuals use a variety of devices for innocuous day-to-day activities; however, there are some malicious individuals (dishonest agents) whose aim is to cause harm, with the exfiltration of information being one of the biggest concerns. Since the security of Wi-Fi communications is one of the areas of greatest investment and research regarding Internet security, dishonest agents make use of side channels to exfiltrate information, namely Bluetooth. Most current solutions for anomaly detection on networks are based on analyzing frames or packets, which, inadvertently, can reveal user behavior patterns, which they consider to be private. In addition, solutions that focus on inspecting physical layer data typically use received signal power (RSSI) as a distance metric and detect anomalies based on the relative position of the network nodes, or use the spectrum values directly on models classification without prior data processing. This Dissertation proposes mechanisms to detect anomalies, while ensuring the privacy of its nodes, which are based on the analysis of radio activity in the physical layer, measuring the behavior of the network through the number of active and inactive frequencies and the duration of periods of silence and activity. After the extraction of properties that characterize these metrics,an exploration and study of the data is carried out, followed by the use of the result to train One-Class Classification models. The models are trained with data taken from a series of interactions between a computer, an AP, and a mobile phone in an environment with reduced noise, in an attempt to simulate a simplified home automation scenario. Then, the models were tested with similar data but containing a compromised node, which periodically sent a file to a local machine via a Bluetooth connection. The data show that, in both situations, it was possible to achieve detection accuracy rates in the order of 75 % and 99 %. This work ends with some ideas of resource work, namely changes in the level of pre-processing, ideas of new tests and how to reduce the percentage of false negatives. Hoje, com o advento da IoT e a resultante fragmentação das tecnologias sem fio, elas trazem não apenas benefícios, mas também preocupações. Diariamente vários indivíduos se comunicam entre si usando vários métodos de comunicação. Os indivíduos usam uma variedade de dispositivos para atividades inócuas do dia-adia; no entanto, existem alguns indivíduos mal-intencionados (agentes desonestos) cujo objetivo é causar danos, sendo a exfiltração de informação uma das maiores preocupações. Sendo a segurança das comunicações Wi-Fi uma das áreas de maior investimento e investigação no que toca a segurança na Internet, os agentes desonestos fazem uso de canais laterais para exfiltrar informação, nomeadamente o Bluetooth. A maioria das soluções atuais para deteção de anomalias em redes baseiam-se em analisar tramas ou pacotes, o que, inadvertidamente, pode revelar padrões de comportamento dos utilizadores, que estes considerem privados. Além disso, as soluções que se focam em inspecionar dados da camada física normalmente usam a potência de sinal recebido (RSSI) como uma métrica de distância e detetam anomalias baseadas na posição relativa dos nós da rede, ou usam os valores do espetro diretamente em modelos de classificação sem prévio tratamento de dados. Esta Dissertação propõe mecanismos para deteção de anomalias, assegurando simultaneamente a privacidade dos seus nós, que se baseiam na análise de atividade rádio na camada física, medindo os comportamentos da rede através do número de frequências ativas e inativas e a duração de períodos de silêncio e atividade. Depois da extração de propriedades que caracterizam estas métricas, é realizada uma exploração dos dados e um estudo das mesmas, sendo depois usadas para treinar modelos de classificação mono-classe. Os modelos são treinados com dados retirados de uma série de interações entre um computador, um AP, e um telemóvel num ambiente com ruído reduzido, numa tentativa de simular um cenário de automação doméstica simplificado. De seguida, os modelos foram testados com dados semelhantes mas contendo um nó comprometido, que periodicamente enviava um ficheiro para uma máquina local através de uma ligação Bluetooth. Os dados mostram que, em ambas as situações, foi possível atingir taxas de precisão de deteção na ordem dos 75% e 99%. Este trabalho finaliza com algumas ideias de trabalho futuro, nomeadamente alterações ao nível do pré-processamento, ideias de novos testes e como diminuir a percentagem de falsos negativos. Mestrado em Engenharia de Computadores e Telemática

The number of cyber attacks is increasing on a daily basis also due to the availability of many tools to compromise hosts, network appliances and Internet of Things devices in a simple and effective manner. Moreover, Crime-as-a-Service business models are becoming popular, thus making cyber security a global concern for home users, institutions, enterprises and organizations. Despite the type and the scope of attacks, the first stage usually involves a reconnaissance phase, which aims at acquiring as much information as possible on the potential victim, e.g., the used hardware, network addressing schemes or personal bits of data. Unfortunately, attackers can now rely upon a vast range of opportunities, since information useful to craft tools or launch social engineering campaigns can be retrieved from publicly accessible databases, online social networks, ad-hoc search engines, or gathered by using a variety of applications like traffic sniffers, port scanners or phishing mechanisms. In this perspective, this work classifies and reviews the existing reconnaissance techniques and presents how they evolved in time. Also, it showcases the main countermeasures and discusses potential future research directions in this area.

This paper analyzes the vulnerability space arising in Trusted Execution Environments (TEEs) when interfacing a trusted enclave application with untrusted, potentially malicious code. Considerable research and industry effort has gone into developing TEE runtime libraries with the purpose of transparently shielding enclave application code from an adversarial environment. However, our analysis reveals that shielding requirements are generally not well-understood in real-world TEE runtime implementations. We expose several sanitization vulnerabilities at the level of the Application Binary Interface (ABI) and the Application Programming Interface (API) that can lead to exploitable memory safety and sidechannel vulnerabilities in the compiled enclave. Mitigation of these vulnerabilities is not as simple as ensuring that pointers are outside enclave memory. In fact, we demonstrate that state-of-the-art mitigation techniques such as Intel’s edger8r, Microsoft’s “deep copy marshalling”, or even memory-safe languages like Rust fail to fully eliminate this attack surface. Our analysis reveals 35 enclave interface sanitization vulnerabilities in 8 major open-source shielding frameworks for Intel SGX, RISC-V, and Sancus TEEs. We practically exploit these vulnerabilities in several attack scenarios to leak secret keys from the enclave or enable remote code reuse. We have responsibly disclosed our findings, leading to 5 designated CVE records and numerous security patches in the vulnerable open-source projects, including the Intel SGX-SDK, Microsoft Open Enclave, Google Asylo, and the Rust compiler.

International audience; The rising number of attacks targeting processors at micro-architecture level encourages more research on hardware level solutions.In this position paper, we specify a new RV32S “secure” instruction set architecture (ISA) derived from the RV32I RISC-V ISA.We propose modifications in the ISA to prevent timing side-channels, strengthen control flow integrity and ensure micro-architectural state isolation.The goal is to provide a new minimal hardware/software approach through which software attacks exploiting hardware vulnerabilities can be circumvented.

We present Rogue In-flight Data Load (RIDL), a new class of speculative unprivileged and constrained attacks to leak arbitrary data across address spaces and privilege boundaries (e.g., process, kernel, SGX, and even CPU-internal operations). Our reverse engineering efforts show such vulnerabilities originate from a variety of micro-optimizations pervasive in commodity (Intel) processors, which cause the CPU to speculatively serve loads using extraneous CPU-internal in-flight data (e.g., in the line fill buffers). Contrary to other state-of-the-art speculative execution attacks, such as Spectre, Meltdown and Foreshadow, RIDL can leak this arbitrary in-flight data with no assumptions on the state of the caches or translation data structures controlled by privileged software. The implications are worrisome. First, RIDL attacks can be implemented even from linear execution with no invalid page faults, eliminating the need for exception suppression mechanisms and enabling system-wide attacks from arbitrary unprivileged code (including JavaScript in the browser). To exemplify such attacks, we build a number of practical exploits that leak sensitive information from victim processes, virtual machines, kernel, SGX and CPU-internal components. Second, and perhaps more importantly, RIDL bypasses all existing 'spot' mitigations in software (e.g., KPTI, PTE inversion) and hardware (e.g., speculative store bypass disable) and cannot easily be mitigated even by more heavyweight defenses (e.g., L1D flushing or disabling SMT). RIDL questions the sustainability of a per-variant, spot mitigation strategy and suggests more fundamental mitigations are needed to contain ever-emerging speculative execution attacks.

Side-channel attacks are an especially dangerous form of attack. In this thesis, we focus on the timing side-channel. A program is said to be constant-time if it is not vulnerable to timing attacks. We present in this thesis two methods relying on static analysis in order to ensure that a program is constant-time. These methods use formal verification in order to gain the highest possible level of assurance by relying on a verified compilation toolchain made up of the CompCert compiler and the Verasco static analyzer. We also propose a proof methodology in order to ensure that a compiler preserves constant-time security during compilation.; Les attaques par canaux cachés sont une forme d'attaque particulièrement dangereuse. Dans cette thèse, nous nous intéressons au canal caché temporel. Un programme est dit ''constant-time'' lorsqu'il n'est pas vulnérable aux attaques par canal caché temporel. Nous présentons dans ce manuscrit deux méthodes reposant sur l'analyse statique afin de s'assurer qu'un programme est constant-time. Ces méthodes se placent dans le cadre de vérification formelle afin d'obtenir le plus haut niveau d'assurance possible en s'appuyant sur une chaîne de compilation vérifiée composée du compilateur CompCert et de l'analyseur statique Verasco. Nous proposons aussi une méthode de preuve afin de s'assurer qu'un compilateur préserve la propriété de constant-time lors de la compilation d'un programme.

International audience; A common security recommendation is to reduce the in-memory lifetime of secret values, in order to reduce the risk that an attacker can obtain secret data by probing memory. To mitigate this risk, secret values can be overwritten, at source level, after their last use. The problem we address here is how to ensure that a compiler preserve these mitigation efforts and thus that secret values are not easier to obtain at assembly level than at source level. We propose a formal definition of Information Flow Preserving program Transformations in which we model the information leak of a program using the notion of Attacker Knowledge. Program transformations are validated by relating the knowledge of the attacker before and after the transformation. We consider two classic compiler passes (Dead Store Elimination and Register Allocation) and show how to validate and, if needed, modify these transformations in order to be information flow preserving.

This work focuses on side-channel resilient design strategies for symmetrickey cryptographic primitives targeting lightweight applications. In light of NIST’s lightweight cryptography project, design choices for block ciphers must consider not only security against traditional cryptanalysis, but also side-channel security, while adhering to low area and power requirements. In this paper, we explore design strategies for substitution-permutation network (SPN)-based block ciphers that make them amenable to low-cost threshold implementations (TI) - a provably secure strategy against side-channel attacks. The core building blocks for our strategy are cryptographically optimal 4×4 S-Boxes, implemented via repeated iterations of simple cellular automata (CA) rules. We present highly optimized TI circuits for such S-Boxes, that consume nearly 40% less area and power as compared to popular lightweight S-Boxes such as PRESENT and GIFT. We validate our claims via implementation results on ASIC using 180nm technology. We also present a comparison of TI circuits for two popular lightweight linear diffusion layer choices - bit permutations and MixColumns using almost-maximum-distance-separable (almost-MDS) matrices. We finally illustrate design paradigms that combine the aforementioned TI circuits for S-Boxes and diffusion layers to obtain fully side-channel secure SPN block cipher implementations with low area and power requirements., IACR Transactions on Symmetric Cryptology, Volume 2018, Issue 3

In recent years, mobile devices (such as smartphones and tablets) have become essential tools in everyday life for billions of people all around the world. Users continuously carry such devices with them and use them for daily communication activities and social network interactions. Hence, such devices contain a huge amount of private and sensitive information. For this reason, mobile devices become popular targets of attacks. In most attack settings, the adversary aims to take local or remote control of a device to access user sensitive information. However, such violations are not easy to carry out since they need to leverage a vulnerability of the system or a careless user (i.e., install a malware app from an unreliable source). A different approach that does not have these shortcomings is the side-channels analysis. In fact, side-channels are physical phenomenon that can be measured from both inside or outside a device. They are mostly due to the user interaction with a mobile device, but also to the context in which the device is used, hence they can reveal sensitive user information such as identity and habits, environment, and operating system itself. Hence, this approach consists of inferring private information that is leaked by a mobile device through a side-channel. Besides, side-channel information is also extremely valuable to enforce security mechanisms such as user authentication, intrusion and information leaks detection. This dissertation investigates novel security and privacy challenges on the analysis of side-channels of mobile devices. This thesis is composed of three parts, each focused on a different side-channel: (i) the usage of network traffic analysis to infer user private information; (ii) the energy consumption of mobile devices during battery recharge as a way to identify a user and as a covert channel to exfiltrate data; and (iii) the possible security application of data collected from built-in sensors in mobile devices to authenticate the user and to evade sandbox detection by malware. In the first part of this dissertation, we consider an adversary who is able to eavesdrop the network traffic of the device on the network side (e.g., controlling a WiFi access point). The fact that the network traffic is often encrypted makes the attack even more challenging. Our work proves that it is possible to leverage machine learning techniques to identify user activity and apps installed on mobile devices analyzing the encrypted network traffic they produce. Such insights are becoming a very attractive data gathering technique for adversaries, network administrators, investigators and marketing agencies. In the second part of this thesis, we investigate the analysis of electric energy consumption. In this case, an adversary is able to measure with a power monitor the amount of energy supplied to a mobile device. In fact, we observed that the usage of mobile device resources (e.g., CPU, network capabilities) directly impacts the amount of energy retrieved from the supplier, i.e., USB port for smartphones, wall-socket for laptops. Leveraging energy traces, we are able to recognize a specific laptop user among a group and detect intruders (i.e., user not belonging to the group). Moreover, we show the feasibility of a covert channel to exfiltrate user data which relies on temporized energy consumption bursts. In the last part of this dissertation, we present a side-channel that can be measured within the mobile device itself. Such channel consists of data collected from the sensors a mobile device is equipped with (e.g., accelerometer, gyroscope). First, we present DELTA, a novel tool that collects data from such sensors, and logs user and operating system events. Then, we develop MIRAGE, a framework that relies on sensors data to enhance sandboxes against malware analysis evasion.

International audience; With the adoption of cloud computing, securing remote program execution becomes an important issue. Relying on standard data encryption is not enough, since code execution happens on remote servers, possibly allowing for eavesdropping from potential adversaries; thus the full execution process requires protection from such threats. In this paper, we introduce OJIT system as a novel approach for obfuscating programs, making it difficult for adversaries to reverse-engineer. The system exploits the JIT compilation technology to dynamically transform the code, making it constantly changing, thereby complicating the execution state. This paper quantitatively studies the effect of this approach by considering a set of obfuscation metrics borrowed from the software engineering field. The paper constructs a testbed system using the LLVM compilation framework that frequently applies random sequences of standard compiler optimizations on the currently running program. Results on using selected benchmarks from the SPEC CPU 2006 suite show a significant sustainable increase in obfuscation for a large number of standard optimizations over the run-time course of the programs.

We present a computer-aided framework for proving concrete security bounds for cryptographic machine code implementations. The front-end of the framework is an interactive verification tool that extends the EasyCrypt framework to reason about relational properties of C-like programs extended with idealised probabilistic operations in the style of code-based security proofs. The framework also incorporates an extension of the CompCert certified compiler to support trusted libraries providing complex arithmetic calculations or instantiating idealized components such as sampling operations. This certified compiler allows us to carry to executable code the security guarantees established at the high-level, and is also instrumented to detect when compilation may interfere with side-channel countermeasures deployed in source code. We demonstrate the applicability of the framework by applying it to the RSA-OAEP encryption scheme, as standard- ized in PKCS#1 v2.1. The outcome is a rigorous analysis of the advantage of an adversary to break the security of as- sembly implementations of the algorithms specified by the standard. The example also provides two contributions of independent interest: it bridges the gap between computer-assisted security proofs and real-world cryptographic implementations as described by standards such as PKCS,and demonstrates the use of the CompCert certified compiler in the context of cryptographic software development., ONR -Office of Naval Research(N000141210914)

This is the journal's version originally published in Journal of Computers: http://dx.doi.org/10.4304/jcp.7.4.827-837. This is an open access journal. Reprinted with permission from Academy Publisher. The energy dissipation associated with switching in CMOS logic gates can be used to classify the microprocessor’s activity. In VLSI design, layout dependent phenomena, such as capacitive crosstalk, become a major contributor to the power consumption and delays of on-chip busses as transistor technology get smaller. These effects may be known to the security community but have received little attention. In a recent paper we presented a new power model, taking into consideration capacitive crosstalk. We have shown that capacitive crosstalk has a significant effect on gate energy dissipation. Our results confirm that the dissipated energy from CMOS switching gates depends not only on the hamming distance (HD), but also on the direction of switching activity on nearby data lines. We show that for an 8 bit data bus, crosstalk may improve detection performance from 2.5 bits (HD based detector) to a theoretical 5.7 bits and simulated 5.0 bits (crosstalk based detector) of information per sample. In this paper we elaborate on the theory and simulations of layout dependent phenomena and how they must be considered when analyzing security implications of power and electromagnetic side-channels. We have also added a small case study, i.e. the electromagnetic side-channel of a smart card, that supports our simulations/theoretical results.