Academic Publications

Why Johnny the Developer Can’t Work with Public Key Certificates

Authors: Martin Ukrop, Vashek Matyáš,

Research cooperation of CRoCS, Faculty of Informatics, Masaryk University and Red Hat. Authors: Martin Ukrop and Vashek Matyas Conference: RSA Cryptographers’ Track 2018 Paper details: Page with PDF and supplementary materials Abstract There have been many studies exposing poor usability of security software for the common end user. However, only a few inspect the usability challenges faced by more knowledgeable users. We conducted an experiment to empirically assess usability of the command line interface of OpenSSL, a well known and widely used cryptographic library. Based on the results, we try to propose specific improvements that would encourage more secure behavior.

Extending Full Disk Encryption for the Future

Authors: Milan Brož,

Full Disk Encryption (FDE) provides confidentiality of a data-at-rest stored on persistent devices like disk or solid state drives (SSD). Typical examples of widely used FDE systems are Bitlocker on Windows, dm-crypt on Linux and Android, TrueCrypt followers or any self-encrypted drives (SED). Our goal is to show that we can extend FDE to use additional metadata conceptually and provide authenticated encryption on this layer without need to modify any layer above the FDE.

The TrueCrypt On-Disk Format—An Independent View

Authors: Milan Brož, Vashek Matyáš,

Full disk encryption (FDE) is a common way to prevent unauthorized use of data by encrypting the whole storage device. TrueCrypt (www.truecrypt.org) is one of the widest-known open source tools providing FDE. It’s available for multiple OSs including Windows, Mac OS, and Linux, letting you share encrypted storage among these systems. Unfortunately, there are license problems and questions related to implementation security. An ongoing community-funded project aims to review license issues and perform a full security audit of source codes (see istruecryptauditedyet.com). We took a different approach.

Selecting a new key derivation function for disk encryption

Authors: Milan Brož, Vashek Matyáš,

Many full disk encryption applications rely on a strong password-based key derivation function to process a passphrase. This article defines requirements for key derivation functions and analyzes recently presented password hashing functions (second round finalists of the Password Hashing Competition) for their suitability for disk encryption.

Weak Memory Models as LLVM-to-LLVM Transformations

Authors: Jiří Barnat, Petr Ročkai, Vladimír Štill,

Data races are among the most difficult software bugs to discover. They arise from multiple threads accessing the same memory location, a situation which is often hard to discern from source code alone. Detection of such bugs is further complicated by individual CPUs’ use of relaxed memory models. As a matter of fact, proving absence of data races is a typical task for automated formal verification. In this paper, we present a new approach for verification of multi-threaded C and C++ programs under weakened memory models (using store buffer emulation), using an unmodified model checker that assumes Sequential Consistency.

Using Off-the-Shelf Exception Support Components in C++ Verification

Authors: Jiří Barnat, Petr Ročkai, Vladimír Štill,

An important step toward adoption of formal methods in software development is support for mainstream programming languages. Unfortunately, these languages are often rather complex and come with substantial standard libraries. However, by choosing a suitable intermediate language, most of the complexity can be delegated to existing execution-oriented (as opposed to verification-oriented) compiler frontends and standard library implementations. In this paper, we describe how support for C++ exceptions can take advantage of the same principle. Our work is based on DiVM, an LLVM-derived, verification-friendly intermediate language.

On Verifying C++ Programs with Probabilities

Authors: Ivana Černá, Jiří Barnat, Kristína Zákopčanová, Petr Ročkai, Vladimír Štill,

In this paper, we report on successful chaining of two unique model checkers, namely DIVINE and PRISM, which, as a whole, allows for practical verification of multi-threaded C++ programs that may choose input and other actions according to a given discrete probabilistic distribution. In the paper, we discuss technical details of the extensions of the DIVINE model checker that were required to enable the chaining, in particular, we report on combination of dynamic τ+reduction used within the DIVINE state space exploration engine with the probabilistic choice operator. We also give preliminary experimental evaluation of our approach, discuss some possible applications […]

Model Checking of C and C++ with DIVINE 4

Authors: Henrich Lauko, Jan Mrázek, Jiří Barnat, Katarína Kejstová, Petr Ročkai, Tadeáš Kučera, Vladimír Štill, Zuzana Baranová,

Abstract: The fourth version of the DIVINE model checker provides a modular platform for verification of real-world programs. It is built around an efficient interpreter of LLVM code which, together with a small, verification-oriented operating system and a set of runtime libraries, enables verification of code written in C and C++.

Model Checking C++ with Exceptions

Authors: Jiří Barnat, Luboš Brim, Petr Ročkai,

We present an extension of the DIVINE software model checker to support programs with exception handling. The extension consists of two parts, a language-neutral implementation of the LLVM exception-handling instructions, and an adaptation of the C++ runtime for the DIVINE/LLVM exception model. This constitutes an important step towards support of both the full C++ specification and towards verification of real-world C++ programs using a software model checker. Additionally, we show how these extensions can be used to elegantly implement other features with non-local control transfer, most importantly the longjmp function in C.

Improved State Space Reductions for LTL Model Checking of C & C++ Programs

Authors: Jiří Barnat, Luboš Brim, Petr Ročkai,

In this paper, we present substantial improvements in efficiency of explicit-state LTL model checking of C & C++ programs, building on [2], including improvements to state representation and to state space reduction techniques. The improved state representation allows to easily exploit symmetries in heap configurations of the program, especially in programs with interleaved heap allocations. Finally, we present a major improvement through a semi-dynamic proviso for partial-order reduction, based on eager local searches constrained through control-flow loop detection.

Fast, Dynamically-Sized Concurrent Hash Table

Authors: Jiří Barnat, Jiří Weiser, Petr Ročkai, Vladimír Štill,

We present a new design and a C++ implementation of a high-performance, cache-efficient hash table suitable for use in implementation of parallel programs in shared memory. Among the main design criteria were the ability to efficiently use variable-length keys, dynamic table resizing to accommodate data sets of unpredictable size and fully concurrent read-write access. We show that the design is correct with respect to data races, both through a high-level argument, as well as by using a model checker to prove crucial safety properties of the actual implementation. Finally, we provide a number of benchmarks showing the performance characteristics of […]

DiVinE: Parallel Distributed Model Checker

Authors: Jiří Barnat, Luboš Brim, Petr Ročkai,

Model checking became a standard method of analyzing complex systems in many application domains. No doubt, a number of applications is placing great demands on model checking tools. The process of analysis of complex and real-life systems often requires vast computation resources, memory in particular. This phenomenon, referred to as the state space explosion problem, has been tackled by many researchers during the past two decades. A plethora of more or less successful techniques to fight the problem have been introduced, including parallel and distributed-memory processing.

DiVinE 3.0 – An Explicit-State Model Checker for Multithreaded C & C++ Programs

Authors: Jan Havlíček, Jan Kriho, Jiří Barnat, Jiří Weiser, Luboš Brim, Milan Lenčo, Petr Ročkai, Vladimír Štill, Vojtěch Havel,

We present a new release of the parallel and distributed LTL model checker DiVinE. The major improvement in this new release is an extension of the class of systems that may be verified with the model checker, while preserving the unique DiVinE feature, namely parallel and distributed-memory processing. Version 3.0 comes with support for direct model checking of (closed) multithreaded C/C++ programs, full untimed-LTL model checking of timed automata, and a general-purpose framework for interfacing with arbitrary system modelling tools.

Context-Switch-Directed Verification in DIVINE

Authors: Jiří Barnat, Petr Ročkai, Vladimír Štill,

In model checking of real-life C and C++ programs, both search efficiency and counterexample readability are very important. In this paper, we suggest context-switch-directed exploration as a way to find a well-readable counterexample faster. Furthermore, we allow to limit the number of context switches used in state-space exploration if desired. The new algorithm is implemented in the DIVINE model checker and enables both unbounded and bounded context-switch-directed ex- ploration for models given in LLVM bitcode, which efficiently allows for verification of multi-threaded C and C++ programs.