2020
Yavuz, Tuba; Bai, Ken (Yihang)
Analyzing system software components using API model guided symbolic execution Journal Article
In: Automated Software Engineering, 2020, ISSN: 1573-7535.
Abstract | Links | BibTeX | Tags: Software Assurance
@article{Yavuz2020b,
title = {Analyzing system software components using API model guided symbolic execution},
author = {Tuba Yavuz and Ken (Yihang) Bai},
url = {https://doi.org/10.1007/s10515-020-00276-5},
doi = {10.1007/s10515-020-00276-5},
issn = {1573-7535},
year = {2020},
date = {2020-09-19},
journal = {Automated Software Engineering},
abstract = {Analyzing real-world software is challenging due to complexity of the software frameworks or APIs they depend on. In this paper, we present a tool, PROMPT, that facilitates the analysisof software components using API model guided symbolic execution. PROMPT has a specification component, PROSE, that lets users define an API model, which consists of a set of data constraints and life-cycle rules that define control-flow constraints among sequentially composed API functions. Given a PROSE model and a software component, PROMPT symbolically executes the component while enforcing the specified API Wmodel. PROMPT has been implemented on top of the KLEE symbolic execution engine and has been applied to Linux device drivers from the video, sound, and network subsystems and to some vulnerable components of BlueZ, the implementation of the Bluetooth protocol stack for the Linux kernel. PROMPT detected two new and four known memory vulnerabilities in some of the analyzed system software components.},
keywords = {Software Assurance},
pubstate = {published},
tppubtype = {article}
}
Analyzing real-world software is challenging due to complexity of the software frameworks or APIs they depend on. In this paper, we present a tool, PROMPT, that facilitates the analysisof software components using API model guided symbolic execution. PROMPT has a specification component, PROSE, that lets users define an API model, which consists of a set of data constraints and life-cycle rules that define control-flow constraints among sequentially composed API functions. Given a PROSE model and a software component, PROMPT symbolically executes the component while enforcing the specified API Wmodel. PROMPT has been implemented on top of the KLEE symbolic execution engine and has been applied to Linux device drivers from the video, sound, and network subsystems and to some vulnerable components of BlueZ, the implementation of the Bluetooth protocol stack for the Linux kernel. PROMPT detected two new and four known memory vulnerabilities in some of the analyzed system software components.
2019
Takarabt, Sofiane; Schaub, Alexander; Facon, Adrien; Guilley, Sylvain; Sauvage, Laurent; Souissi, Youssef; Mathieu, Yves
Cache-Timing Attacks Still Threaten IoT Devices Proceedings Article
In: Codes, Cryptology and Information Security, pp. 13–30, Springer International Publishing, Cham, 2019, ISBN: 978-3-030-16458-4.
Abstract | Links | BibTeX | Tags: Software Assurance
@inproceedings{Takarabt2019Cache,
title = {Cache-Timing Attacks Still Threaten IoT Devices},
author = {Sofiane Takarabt and Alexander Schaub and Adrien Facon and Sylvain Guilley and Laurent Sauvage and Youssef Souissi and Yves Mathieu},
doi = {10.1007/978-3-030-16458-4_2},
isbn = {978-3-030-16458-4},
year = {2019},
date = {2019-01-01},
booktitle = {Codes, Cryptology and Information Security},
pages = {13--30},
publisher = {Springer International Publishing},
address = {Cham},
abstract = {Deployed widely and embedding sensitive data, The security of IoT devices depend on the reliability of cryptographic libraries to protect user information. However when implemented on real systems, cryptographic algorithms are vulnerable to side-channel attacks based on their execution behavior, which can be revealed by measurements of physical quantities such as timing or power consumption. Some countermeasures can be implemented in order to prevent those attacks. However those countermeasures are generally designed at high level description, and when implemented, some residual leakage may persist. In this article we propose a methodology to assess the robustness of the MbedTLS library against timing and cache-timing attacks. This comprehensive study of side-channel security allows us to identify the most frequent weaknesses in software cryptographic code and how those might be fixed. This methodology checks the whole source code, from the top level routines to low level primitives, that are used for the final application. We retrieve hundreds of lines of code that leak sensitive information.},
keywords = {Software Assurance},
pubstate = {published},
tppubtype = {inproceedings}
}
Deployed widely and embedding sensitive data, The security of IoT devices depend on the reliability of cryptographic libraries to protect user information. However when implemented on real systems, cryptographic algorithms are vulnerable to side-channel attacks based on their execution behavior, which can be revealed by measurements of physical quantities such as timing or power consumption. Some countermeasures can be implemented in order to prevent those attacks. However those countermeasures are generally designed at high level description, and when implemented, some residual leakage may persist. In this article we propose a methodology to assess the robustness of the MbedTLS library against timing and cache-timing attacks. This comprehensive study of side-channel security allows us to identify the most frequent weaknesses in software cryptographic code and how those might be fixed. This methodology checks the whole source code, from the top level routines to low level primitives, that are used for the final application. We retrieve hundreds of lines of code that leak sensitive information.
Carré, Sébastien; Facon, Adrien; Guilley, Sylvain; Takarabt, Sofiane; Schaub, Alexander; Souissi, Youssef
Cache-Timing Attack Detection and Prevention Proceedings Article
In: Constructive Side-Channel Analysis and Secure Design, pp. 13–21, Springer International Publishing, Cham, 2019, ISBN: 978-3-030-16350-1.
Abstract | Links | BibTeX | Tags: Software Assurance
@inproceedings{Carre2019Cache,
title = {Cache-Timing Attack Detection and Prevention},
author = {Sébastien Carré and Adrien Facon and Sylvain Guilley and Sofiane Takarabt and Alexander Schaub and Youssef Souissi},
doi = {10.1007/978-3-030-16350-1_2},
isbn = {978-3-030-16350-1},
year = {2019},
date = {2019-01-01},
booktitle = {Constructive Side-Channel Analysis and Secure Design},
pages = {13--21},
publisher = {Springer International Publishing},
address = {Cham},
abstract = {With the publication of Spectre & Meltdown attacks, cache-timing exploitation techniques have received a wealth of attention recently. On the one hand, it is now well understood which patterns in the source code create observable unbalances in terms of timing. On the other hand, some practical attacks have also been reported. But the exact relation between vulnerabilities and exploitations is not enough studied as of today. In this article, we put forward a methodology to characterize the leakage induced by a ``non-constant-time'' construct in the source code. This methodology allows us to recover known attacks and to warn about possible new ones, possibly devastating.},
keywords = {Software Assurance},
pubstate = {published},
tppubtype = {inproceedings}
}
With the publication of Spectre & Meltdown attacks, cache-timing exploitation techniques have received a wealth of attention recently. On the one hand, it is now well understood which patterns in the source code create observable unbalances in terms of timing. On the other hand, some practical attacks have also been reported. But the exact relation between vulnerabilities and exploitations is not enough studied as of today. In this article, we put forward a methodology to characterize the leakage induced by a ``non-constant-time'' construct in the source code. This methodology allows us to recover known attacks and to warn about possible new ones, possibly devastating.
Bruneau, Nicolas; Christen, Charles; Danger, Jean-Luc; Facon, Adrien; Guilley, Sylvain
Security Evaluation Against Side-Channel Analysis at Compilation Time Proceedings Article
In: pp. 129–148, Springer International Publishing, Cham, 2019, ISBN: 978-3-030-36237-9.
Abstract | Links | BibTeX | Tags: Software Assurance
@inproceedings{Bruneau2019security,
title = {Security Evaluation Against Side-Channel Analysis at Compilation Time},
author = {Nicolas Bruneau and Charles Christen and Jean-Luc Danger and Adrien Facon and Sylvain Guilley},
doi = {10.1007/978-3-030-36237-9_8},
isbn = {978-3-030-36237-9},
year = {2019},
date = {2019-01-01},
pages = {129--148},
publisher = {Springer International Publishing},
address = {Cham},
abstract = {Masking countermeasure is implemented to thwart side-channel attacks. The maturity of high-order masking schemes has reached the level where the concepts are sound and proven. For instance, Rivain and Prouff proposed a full-fledged AES at CHES 2010. Some non-trivial fixes regarding refresh functions were needed though. Now, industry is adopting such solutions, and for the sake of both quality and certification requirements, masked cryptographic code shall be checked for correctness using the same model as that of the theoretical protection rationale (for instance the probing leakage model).},
keywords = {Software Assurance},
pubstate = {published},
tppubtype = {inproceedings}
}
Masking countermeasure is implemented to thwart side-channel attacks. The maturity of high-order masking schemes has reached the level where the concepts are sound and proven. For instance, Rivain and Prouff proposed a full-fledged AES at CHES 2010. Some non-trivial fixes regarding refresh functions were needed though. Now, industry is adopting such solutions, and for the sake of both quality and certification requirements, masked cryptographic code shall be checked for correctness using the same model as that of the theoretical protection rationale (for instance the probing leakage model).