Subscribe to the gold package and get unlimited access to Shamra Academy
Register a new userMetaCP: Cryptographic Protocol Design Tool for Formal Verification
107
0
0.0
(
0
)
Added by
Roberto Metere
Publication date
2021
fields
Informatics Engineering
and research's language is
English
Ask ChatGPT about the research
No Arabic abstract
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.
rate research
Read More
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.
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.
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.
NEO is one of the top public chains worldwide. We focus on its backbone consensus protocol, called delegated Byzantine Fault Tolerance (dBFT). The dBFT protocol has been adopted by a variety of blockchain systems such as ONT. dBFT claims to guarantee the security when no more than $f = lfloor frac{n}{3} rfloor$ nodes are Byzantine, where $n$ is the total number of consensus participants. However, we identify attacks to break the claimed security. In this paper, we show our results by providing a security analysis on its dBFT protocol. First, we evaluate NEOs source code and formally present the procedures of dBFT via the state machine replication (SMR) model. Next, we provide a theoretical analysis with two example attacks. These attacks break the security of dBFT with no more than $f$ nodes. Then, we provide recommendations on how to fix the system against the identified attacks. The suggested fixes have been accepted by the NEO official team. Finally, we further discuss the reasons causing such issues, the relationship with current permissioned blockchain systems, and the scope of potential influence.
In this paper, we propose a blockchain-based computing verification protocol, called EntrapNet, for distributed shared computing networks, an emerging underlying network for many internet of things (IoT) applications. EntrapNet borrows the idea from the practice of entrapment in criminal law to reduce the possibility of receiving incorrect computing results from trustless service providers who have offered the computing resources. Furthermore, we mathematically optimize EntrapNet to deal with the fundamental tradeoff of a network: security and efficiency. We present an asymptotic optimal solution to this optimization. It will be seen that EntrapNet can be performed as an independent and low-cost layer atop any trustless network that requires outsourced computing, thus making secure computing affordable and practical.
Log in to be able to interact and post comments
comments
Fetching comments
Sign in to be able to follow your search criteria
