Subscribe to the gold package and get unlimited access to Shamra Academy
Register a new userVivienne: Relational Verification of Cryptographic Implementations in WebAssembly
174
0
0.0
(
0
)
Added by
Rodothea Myrsini Tsoupidi
Publication date
2021
fields
Informatics Engineering
and research's language is
English
Ask ChatGPT about the research
No Arabic abstract
This paper explores the use of relational symbolic execution to counter timing side channels in WebAssembly programs. We design and implement Vivienne, an open-source tool to automatically analyze WebAssembly cryptographic libraries for constant-time violations. Our approach features various optimizations that leverage the structure of WebAssembly and automated theorem provers, including support for loops via relational invariants. We evaluate Vivienne on 57 real-world cryptographic implementations, including a previously unverified implementation of the HACL* library in WebAssembly. The results indicate that Vivienne is a practical solution for constant-time analysis of cryptographic libraries in WebAssembly.
rate research
Read More
Internet of Things (IoT) consists of a large number of devices connected through a network, which exchange a high volume of data, thereby posing new security, privacy, and trust issues. One way to address these issues is ensuring data confidentiality using lightweight encryption algorithms for IoT protocols. However, the design and implementation of such protocols is an error-prone task; flaws in the implementation can lead to devastating security vulnerabilities. Here we propose a new verification approach named Encryption-BMC and Fuzzing (EBF), which combines Bounded Model Checking (BMC) and Fuzzing techniques to check for security vulnerabilities that arise from concurrent implementations of cyrptographic protocols, which include data race, thread leak, arithmetic overflow, and memory safety. EBF models IoT protocols as a client and server using POSIX threads, thereby simulating both entities communication. It also employs static and dynamic verification to cover the systems state-space exhaustively. We evaluate EBF against three benchmarks. First, we use the concurrency benchmark from SV-COMP and show that it outperforms other state-of-the-art tools such as ESBMC, AFL, Lazy-CSeq, and TSAN with respect to bug finding. Second, we evaluate an open-source implementation called WolfMQTT. It is an MQTT client implementation that uses the WolfSSL library. We show that tool detects a data race bug, which other approaches are unable to find. Third, to show the effectiveness of EBF, we replicate some known vulnerabilities in OpenSSL and CyaSSL (lately WolfSSL) libraries. EBF can detect the bugs in minimum time.
We present MetaCP, a tool to aid the cryptographer throughout the process of designing and modelling a communication protocol suitable for formal verification. The crucial innovative aspect of the tool is its data-centric approach, where protocol specification is stored in a structured way rather than in natural languages to facilitate its interpretation to multiple target languages. Previous work shows a single exporting plugin (for Tamarin) which required aftermath modifications. By improving the expressiveness of the specification data structure we extend the tool to export to an additional formal language, i.e. ProVerif, as well as a C++ implementation. Starting with its modern graphical interface, MetaCP allows us to model the Diffie-Hellman key exchange, traditionally referred to as a case study, in just a few minutes. Ultimately, we use the formal tools to verify the executability and correctness of the automatically exported models. The design core of MetaCP is freely available in an online demo that provides two further sample protocols, Needham-Schroeder and Needham-Schroeder-Lowe, along with instructions to use the tool to begin modelling from scratch and to export the model to desired external languages.
The proceedings consist of a keynote paper by Alberto followed by 6 invited papers written by Lorenzo Clemente (U. Warsaw), Alain Finkel (U. Paris-Saclay), John Gallagher (Roskilde U. and IMDEA Software Institute) et al., Neil Jones (U. Copenhagen) et al., Michael Leuschel (Heinrich-Heine U.) and Maurizio Proietti (IASI-CNR) et al.. These invited papers are followed by 4 regular papers accepted at VPT 2020 and the papers of HCVS 2020 which consist of three contributed papers and an invited paper on the third competition of solvers for Constrained Horn Clauses. In addition, the abstracts (in HTML format) of 3 invited talks at VPT 2020 by Andrzej Skowron (U. Warsaw), Sophie Renault (EPO) and Moa Johansson (Chalmers U.), are included.
The Secure Sockets Layer (SSL) and Transport Layer Security (TLS) protocols are the foundation of network security. The certificate verification in SSL/TLS implementations is vital and may become the weak link in the whole network ecosystem. In previous works, some research focused on the automated testing of certificate verification, and the main approaches rely on generating massive certificates through randomly combining parts of seed certificates for fuzzing. Although the generated certificates could meet the semantic constraints, the cost is quite heavy, and the performance is limited due to the randomness. To fill this gap, in this paper, we propose DRLGENCERT, the first framework of applying deep reinforcement learning to the automated testing of certificate verification in SSL/TLS implementations. DRLGENCERT accepts ordinary certificates as input and outputs newly generated certificates which could trigger discrepancies with high efficiency. Benefited by the deep reinforcement learning, when generating certificates, our framework could choose the best next action according to the result of a previous modification, instead of simple random combinations. At the same time, we developed a set of new techniques to support the overall design, like new feature extraction method for X.509 certificates, fine-grained differential testing, and so forth. Also, we implemented a prototype of DRLGENCERT and carried out a series of real-world experiments. The results show DRLGENCERT is quite efficient, and we obtained 84,661 discrepancy-triggering certificates from 181,900 certificate seeds, say around 46.5% effectiveness. Also, we evaluated six popular SSL/TLS implementations, including GnuTLS, MatrixSSL, MbedTLS, NSS, OpenSSL, and wolfSSL. DRLGENCERT successfully discovered 23 serious certificate verification flaws, and most of them were previously unknown.
We propose MetaCP, a Meta Cryptography Protocol verification tool, as an automated tool simplifying the design of security protocols through a graphical interface. The graphical interface can be seen as a modern editor of a non-relational database whose data are protocols. The information of protocols are stored in XML, enjoying a fixed format and syntax aiming to contain all required information to specify any kind of protocol. This XML can be seen as an almost semanticless language, where different plugins confer strict semantics modelling the protocol into a variety of back-end verification languages. In this paper, we showcase the effectiveness of this novel approach by demonstrating how easy MetaCP makes it to design and verify a protocol going from the graphical design to formally verified protocol using a Tamarin prover plugin. Whilst similar approaches have been proposed in the past, most famously the AVISPA Tool, no previous approach provides such as small learning curve and ease of use even for non security professionals, combined with the flexibility to integrate with the state of the art verification tools.
Log in to be able to interact and post comments
comments
Fetching comments
Sign in to be able to follow your search criteria
