Showing 1–9 of 9 results for author: Lindner, A

Beyond Over-Protection: A Targeted Approach to Spectre Mitigation and Performance Optimization

Authors: Tiziano Marinaro, Pablo Buiras, Andreas Lindner, Roberto Guanciale, Hamed Nemati

Abstract: Since the advent of Spectre attacks, researchers and practitioners have developed a range of hardware and software measures to counter transient execution attacks. A prime example of such mitigation is speculative load hardening in LLVM, which protects against leaks by tracking the speculation state and masking values during misspeculation. LLVM relies on static analysis to harden programs using s… ▽ More Since the advent of Spectre attacks, researchers and practitioners have developed a range of hardware and software measures to counter transient execution attacks. A prime example of such mitigation is speculative load hardening in LLVM, which protects against leaks by tracking the speculation state and masking values during misspeculation. LLVM relies on static analysis to harden programs using slh that often results in over-protection, which incurs performance overhead. We extended an existing side-channel model validation framework, Scam-V, to check the vulnerability of programs to Spectre-PHT attacks and optimize the protection of programs using the slh approach. We illustrate the efficacy of Scam-V by first demonstrating that it can automatically identify Spectre vulnerabilities in real programs, e.g., fragments of crypto-libraries. We then develop an optimization mechanism that validates the necessity of slh hardening w.r.t. the target platform. Our experiments showed that hardening introduced by LLVM in most cases could be significantly improved when the underlying microarchitecture properties are considered. △ Less

Submitted 15 December, 2023; originally announced December 2023.

Comments: The paper will appear in ACM AsiaCCS 2024

Proof-Producing Symbolic Execution for Binary Code Verification

Authors: Andreas Lindner, Roberto Guanciale, Mads Dam

Abstract: We propose a proof-producing symbolic execution for verification of machine-level programs. The analysis is based on a set of core inference rules that are designed to give control over the tradeoff between preservation of precision and the introduction of overapproximation to make the application to real world code useful and tractable. We integrate our symbolic execution in a binary analysis pla… ▽ More We propose a proof-producing symbolic execution for verification of machine-level programs. The analysis is based on a set of core inference rules that are designed to give control over the tradeoff between preservation of precision and the introduction of overapproximation to make the application to real world code useful and tractable. We integrate our symbolic execution in a binary analysis platform that features a low-level intermediate language enabling the application of analyses to many different processor architectures. The overall framework is implemented in the theorem prover HOL4 to be able to obtain highly trustworthy verification results. We demonstrate our approach to establish sound execution time bounds for a control loop program implemented for an ARM Cortex-M0 processor. △ Less

Submitted 18 April, 2023; originally announced April 2023.

Speculative Leakage in ARM Cortex-A53

Authors: Hamed Nemati, Roberto Guanciale, Pablo Buiras, Andreas Lindner

Abstract: The recent Spectre attacks have demonstrated that modern microarchitectural optimizations can make software insecure. These attacks use features like pipelining, out-of-order and speculation to extract information about the memory contents of a process via side-channels. In this paper we demonstrate that Cortex-A53 is affected by speculative leakage even if the microarchitecture does not support o… ▽ More The recent Spectre attacks have demonstrated that modern microarchitectural optimizations can make software insecure. These attacks use features like pipelining, out-of-order and speculation to extract information about the memory contents of a process via side-channels. In this paper we demonstrate that Cortex-A53 is affected by speculative leakage even if the microarchitecture does not support out-of-order execution. We named this new class of vulnerabilities SiSCloak. △ Less

Submitted 17 July, 2020; v1 submitted 14 July, 2020; originally announced July 2020.

Validation of Abstract Side-Channel Models for Computer Architectures

Authors: Hamed Nemati, Pablo Buiras, Andreas Lindner, Roberto Guanciale, Swen Jacobs

Abstract: Observational models make tractable the analysis of information flow properties by providing an abstraction of side channels. We introduce a methodology and a tool, Scam-V, to validate observational models for modern computer architectures. We combine symbolic execution, relational analysis, and different program generation techniques to generate experiments and validate the models. An experiment… ▽ More Observational models make tractable the analysis of information flow properties by providing an abstraction of side channels. We introduce a methodology and a tool, Scam-V, to validate observational models for modern computer architectures. We combine symbolic execution, relational analysis, and different program generation techniques to generate experiments and validate the models. An experiment consists of a randomly generated program together with two inputs that are observationally equivalent according to the model under the test. Validation is done by checking indistinguishability of the two inputs on real hardware by executing the program and analyzing the side channel. We have evaluated our framework by validating models that abstract the data-cache side channel of a Raspberry Pi 3 board with a processor implementing the ARMv8-A architecture. Our results show that Scam-V can identify bugs in the implementation of the models and generate test programs which invalidate the models due to hidden microarchitectural behavior. △ Less

Submitted 11 May, 2020; originally announced May 2020.

Leveraging Implicit Expert Knowledge for Non-Circular Machine Learning in Sepsis Prediction

Authors: Shigehiko Schamoni, Holger A. Lindner, Verena Schneider-Lindner, Manfred Thiel, Stefan Riezler

Abstract: Sepsis is the leading cause of death in non-coronary intensive care units. Moreover, a delay of antibiotic treatment of patients with severe sepsis by only few hours is associated with increased mortality. This insight makes accurate models for early prediction of sepsis a key task in machine learning for healthcare. Previous approaches have achieved high AUROC by learning from electronic health r… ▽ More Sepsis is the leading cause of death in non-coronary intensive care units. Moreover, a delay of antibiotic treatment of patients with severe sepsis by only few hours is associated with increased mortality. This insight makes accurate models for early prediction of sepsis a key task in machine learning for healthcare. Previous approaches have achieved high AUROC by learning from electronic health records where sepsis labels were defined automatically following established clinical criteria. We argue that the practice of incorporating the clinical criteria that are used to automatically define ground truth sepsis labels as features of severity scoring models is inherently circular and compromises the validity of the proposed approaches. We propose to create an independent ground truth for sepsis research by exploiting implicit knowledge of clinical practitioners via an electronic questionnaire which records attending physicians' daily judgements of patients' sepsis status. We show that despite its small size, our dataset allows to achieve state-of-the-art AUROC scores. An inspection of learned weights for standardized features of the linear model lets us infer potentially surprising feature contributions and allows to interpret seemingly counterintuitive findings. △ Less

Submitted 20 September, 2019; originally announced September 2019.

Comments: Accepted for publication in Journal of Artificial Intelligence in Medicine

Journal ref: Artificial Intelligence in Medicine, Volume 100, September 2019, Pages 101725

A survival model for course-course interactions in a Massive Open Online Course platform

Authors: Edwin H. Wintermute, Matthieu Cisel, Ariel B. Lindner

Abstract: Massive Open Online Course (MOOC) platforms incorporate large course catalogs from which individual students may register multiple courses. We performed a network-based analysis of student achievement, considering how course-course interactions may positively or negatively affect student success. Our dataset included 378,000 users and 1,000,000 unique registration events in France Universite Numer… ▽ More Massive Open Online Course (MOOC) platforms incorporate large course catalogs from which individual students may register multiple courses. We performed a network-based analysis of student achievement, considering how course-course interactions may positively or negatively affect student success. Our dataset included 378,000 users and 1,000,000 unique registration events in France Universite Numerique (FUN), a national MOOC platform. We adapt reliability theory to model certificate completion rates with a Weibull survival function, following the intuition that students "survive" in a course for a certain time before stochastically drop** out. Course-course interactions are found to be well described by a single parameter for user engagement that can be estimated from a user's registration profile. User engagement, in turn, correlates with certificate rates in all courses regardless of specific content. The reliability approach is shown to capture several certificate rate patterns that are overlooked by conventional regression models. User engagement emerges as a natural metric for tracking student progress across demographics and over time. △ Less

Submitted 10 May, 2019; originally announced May 2019.

Comments: 6 pages

ACM Class: K.3.0

TrABin: Trustworthy Analyses of Binaries

Authors: Andreas Lindner, Roberto Guanciale, Roberto Metere

Abstract: Verification of microkernels, device drivers, and crypto routines requires analyses at the binary level. In order to automate these analyses, in the last years several binary analysis platforms have been introduced. These platforms share a common design: the adoption of hardware-independent intermediate representations, a mechanism to translate architecture dependent code to this representation, a… ▽ More Verification of microkernels, device drivers, and crypto routines requires analyses at the binary level. In order to automate these analyses, in the last years several binary analysis platforms have been introduced. These platforms share a common design: the adoption of hardware-independent intermediate representations, a mechanism to translate architecture dependent code to this representation, and a set of architecture independent analyses that process the intermediate representation. The usage of these platforms to verify software introduces the need for trusting both the correctness of the translation from binary code to intermediate language (called transpilation) and the correctness of the analyses. Achieving a high degree of trust is challenging since the transpilation must handle (i) all the side effects of the instructions, (ii) multiple instruction encodings (e.g. ARM Thumb), and (iii) variable instruction length (e.g. Intel). Similarly, analyses can use complex transformations (e.g. loop unrolling) and simplifications (e.g. partial evaluation) of the artifacts, whose bugs can jeopardize correctness of the results. We overcome these problems by develo** a binary analysis platform on top of the interactive theorem prover HOL4. First, we formally model a binary intermediate language and we prove correctness of several supporting tools (i.e. a type checker). Then, we implement two proof-producing transpilers, which respectively translate ARMv8 and CortexM0 programs to the intermediate language and generate a certificate. This certificate is a HOL4 proof demonstrating correctness of the translation. As demonstrating analysis, we implement a proof-producing weakest precondition generator, which can be used to verify that a given loop-free program fragment satisfies a contract. Finally, we use an AES encryption implementation to benchmark our platform. △ Less

Submitted 16 January, 2019; originally announced January 2019.

Comments: 32 pages, 5 figures, journal. arXiv admin note: substantial text overlap with arXiv:1807.10664

Sound Transpilation from Binary to Machine-Independent Code

Authors: Roberto Metere, Andreas Lindner, Roberto Guanciale

Abstract: In order to handle the complexity and heterogeneity of mod- ern instruction set architectures, analysis platforms share a common design, the adoption of hardware-independent intermediate representa- tions. The usage of these platforms to verify systems down to binary-level is appealing due to the high degree of automation they provide. How- ever, it introduces the need for trusting the correctness… ▽ More In order to handle the complexity and heterogeneity of mod- ern instruction set architectures, analysis platforms share a common design, the adoption of hardware-independent intermediate representa- tions. The usage of these platforms to verify systems down to binary-level is appealing due to the high degree of automation they provide. How- ever, it introduces the need for trusting the correctness of the translation from binary code to intermediate language. Achieving a high degree of trust is challenging since this transpilation must handle (i) all the side effects of the instructions, (ii) multiple instruction encoding (e.g. ARM Thumb), and (iii) variable instruction length (e.g. Intel). We overcome these problems by formally modeling one of such intermediate languages in the interactive theorem prover HOL4 and by implementing a proof- producing transpiler. This tool translates ARMv8 programs to the in- termediate language and generates a HOL4 proof that demonstrates the correctness of the translation in the form of a simulation theorem. We also show how the transpiler theorems can be used to transfer properties verified on the intermediate language to the binary code. △ Less

Submitted 27 July, 2018; originally announced July 2018.

Localization of protein aggregation in Escherichia coli is governed by diffusion and nucleoid macromolecular crowding effect

Authors: Anne-Sophie Coquel, Jean-Pascal Jacob, Maël Primet, Alice Demarez, Mariella Dimiccoli, Thomas Julou, Lionel Moisan, Ariel B. Lindner, Hugues Berry

Abstract: Aggregates of misfolded proteins are a hallmark of many age-related diseases. Recently, they have been linked to aging of Escherichia coli (E. coli) where protein aggregates accumulate at the old pole region of the aging bacterium. Because of the potential of E. coli as a model organism, elucidating aging and protein aggregation in this bacterium may pave the way to significant advances in our glo… ▽ More Aggregates of misfolded proteins are a hallmark of many age-related diseases. Recently, they have been linked to aging of Escherichia coli (E. coli) where protein aggregates accumulate at the old pole region of the aging bacterium. Because of the potential of E. coli as a model organism, elucidating aging and protein aggregation in this bacterium may pave the way to significant advances in our global understanding of aging. A first obstacle along this path is to decipher the mechanisms by which protein aggregates are targeted to specific intercellular locations. Here, using an integrated approach based on individual-based modeling, time-lapse fluorescence microscopy and automated image analysis, we show that the movement of aging-related protein aggregates in E. coli is purely diffusive (Brownian). Using single-particle tracking of protein aggregates in live E. coli cells, we estimated the average size and diffusion constant of the aggregates. Our results evidence that the aggregates passively diffuse within the cell, with diffusion constants that depend on their size in agreement with the Stokes-Einstein law. However, the aggregate displacements along the cell long axis are confined to a region that roughly corresponds to the nucleoid-free space in the cell pole, thus confirming the importance of increased macromolecular crowding in the nucleoids. We thus used 3d individual-based modeling to show that these three ingredients (diffusion, aggregation and diffusion hindrance in the nucleoids) are sufficient and necessary to reproduce the available experimental data on aggregate localization in the cells. Taken together, our results strongly support the hypothesis that the localization of aging-related protein aggregates in the poles of E. coli results from the coupling of passive diffusion- aggregation with spatially non-homogeneous macromolecular crowding. They further support the importance of "soft" intracellular structuring (based on macromolecular crowding) in diffusion-based protein localization in E. coli. △ Less

Submitted 8 March, 2013; originally announced March 2013.

Comments: PLoS Computational Biology (2013)