• All authors

  • Reset filters

Will You Trust This TLS Certificate? Perceptions of People Working in IT

Research cooperation of CRoCS, Faculty of Informatics, Masaryk University and Red Hat. Authors: Martin Ukrop, Lydia Kraus, Vashek Matyas and Heider Wahsheh Conference: Annual Computer Security Applications Conference (ACSAC) 2019 Paper details: Page with PDF and supplementary materials Abstract Flawed TLS certificates are not uncommon on the Internet. While they signal a potential issue, in most cases they have benign causes (e.g., misconfiguration or even deliberate deployment). This adds fuzziness to the decision on whether to trust a connection or not. Little is known about perceptions of flawed certificates by IT professionals, even though their decisions impact high numbers of […]

November 30, 2019

Lydia KrausMartin UkropVashek Matyáš

Red Hat Research Day

Download file: Red Hat Research Day-program

May 3, 2019

Hugh Brock

The eXpress Data Path: Fast Programmable Packet Processing in the Operating System Kernel

Programmable packet processing is increasingly implemented using kernel bypass  techniques, where a userspace application takes complete control of the  networking hardware to avoid expensive context switches between kernel and  userspace. However, as the operating system is bypassed, so are its  application isolation and security mechanisms; and well-tested configuration,  deployment and management tools cease to function. To overcome this limitation, we present the design of a novel approach to  programmable packet processing, called the eXpress Data Path (XDP). In XDP,  the operating system kernel itself provides a safe execution environment for  custom packet processing applications, executed in device driver context. XDP  […]

March 7, 2019

Daniel BorkmannDavid AhernDavid MillerJesper Dangaard BrouerJohn FastabendToke Høiland-JørgensenTom Herbert

Reflective Diary for Professional Development of Novice Teachers

Many starting teachers of computer science have great professional skill but often lack pedagogical training. Since providing expert mentorship directly during their lessons would be quite costly, institutions usually offer separate teacher training sessions for novice instructors. However, the reflection on teaching performed with a significant delay after the taught lesson limits the possible impact on teachers. To bridge this gap, we introduced a weekly semi-structured reflective practice to supplement the teacher training sessions at our faculty. We created a paper diary that guides the starting teachers through the process of reflection. Over the course of the semester, the diary […]

November 8, 2018

Jan NehybaMartin UkropValdemar Švábenský

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

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.

February 6, 2018

Martin UkropVashek Matyáš

Extending Full Disk Encryption for the Future

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.

December 17, 2017

Milan Brož

The TrueCrypt On-Disk Format—An Independent View

Full disk encryption (FDE) is a common way to prevent unauthorized use of data by encrypting the whole storage device. TrueCrypt ( 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 We took a different approach.

November 27, 2017

Milan BrožVashek Matyáš

Selecting a new key derivation function for disk encryption

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.

Milan BrožVashek Matyáš

Weak Memory Models as LLVM-to-LLVM Transformations

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.

November 14, 2017

Jiří BarnatPetr RočkaiVladimír Štill

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

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.

Jiří BarnatPetr RočkaiVladimír Štill

On Verifying C++ Programs with Probabilities

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 […]

Ivana ČernáJiří BarnatKristína ZákopčanováPetr RočkaiVladimír Štill

Model Checking of C and C++ with DIVINE 4

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++.

Henrich LaukoJan MrázekJiří BarnatKatarína KejstováPetr RočkaiTadeáš KučeraVladimír ŠtillZuzana Baranová

Model Checking C++ with Exceptions

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.

Jiří BarnatLuboš BrimPetr Ročkai

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

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.

Jiří BarnatLuboš BrimPetr Ročkai

Fast, Dynamically-Sized Concurrent Hash Table

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 […]

Jiří BarnatJiří WeiserPetr RočkaiVladimír Štill

DiVinE: Parallel Distributed Model Checker

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.

Jiří BarnatLuboš BrimMilan ČeškaPetr Ročkai

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

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.

Jan HavlíčekJan KrihoJiří BarnatJiří WeiserLuboš BrimMilan LenčoPetr RočkaiVladimír ŠtillVojtěch Havel

Context-Switch-Directed Verification in DIVINE

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.

November 8, 2017

Jiří BarnatPetr RočkaiVladimír Štill