Publications
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
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
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
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
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 (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.
November 27, 2017
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.
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
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.
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 […]
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++.
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.
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.
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 […]
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.
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.
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