Publications

Red Hat Research collaborates with universities and government agencies to produce papers that bring open source contributions along with them.  We also publish informative articles about many of our projects in our own journal, the Red Hat Research Quarterly.

Latest Publications

Explore these publications which are the result of cooperation between Red Hat Research and the Academic sector around the globe focused on open research.

SelfD: Self-Learning Large-Scale Driving Policies From the Web

Abstract: Effectively utilizing the vast amounts of ego-centric navigation data that is freely available on the internet can advance generalized intelligent systems, i.e., to robustly scale across perspectives, platforms, environmental conditions, scenarios, and...

PublicationSummaryUniversitiesCollaborationsInstituteshf:tax:partner_university
Identifying Mismatches Between Microservice Testbeds and Industrial Perceptions of Microservices

Abstract Industrial microservice architectures vary so wildly in their characteristics, such as size or communication method, that comparing systems is …

, emory-university tufts-university
Endure: A Robust Tuning Paradigm for LSM Trees Under Workload Uncertainty

Abstract: Log-Structured Merge trees (LSM trees) are increasingly used as the storage engines behind several data systems, frequently deployed in …

boston-university
SelfD: Self-Learning Large-Scale Driving Policies From the Web

Abstract: Effectively utilizing the vast amounts of ego-centric navigation data that is freely available on the internet can advance generalized …

boston-university
Design and Analysis of Microworlds and Puzzles for Block-Based Programming

Block-based programming is a popular approach to teaching introductory programming. Block-based programming often works in the context of microworlds, where students solve specific puzzles. It is used, for example, within the Hour of Code event, which targets millions of students.

masaryk-university
Motif Mining: Finding and Summarizing Remixed Image Content

On the internet, images are no longer static; they have become dynamic content. Thanks to the availability of smartphones with …

university-of-notre-dame
E-WarP: A System-wide Framework for Memory Bandwidth Profiling and Management

The proliferation of multi-core, accelerator-enabled embedded systems has introduced new opportunities to consolidate real-time systems of increasing complexity. But the …

boston-university
FPGA HPC using OpenCL: Case Study in 3D FFT

FPGAs have typically achieved high speedups for 3D Fast Fourier Transforms (FFTs) due to the presence of hard floating point …

boston-university
Unlocking Performance-Programmability by Penetrating the Intel FPGA OpenCL Toolflow

Improved support for OpenCL has been an important step towards the mainstream adoption of FPGAs as compute resources. Current research …

boston-university
An Empirically Guided Optimization Framework for FPGA OpenCL

FPGAs have been demonstrated to be capable of very high performance, especially power-performance, but generally at the cost of hand-tuned …

boston-university
Towards Hardware as a Reconfigurable, Elastic, and Specialized Service

As modern Data Center workloads become increasingly complex, constrained, and critical, mainstream CPU-centric computing has had ever more difficulty in …

boston-university
Secret Sharing MPC on FPGAs in the Datacenter

Multi-Party Computation (MPC) is a technique enabling data from several sources to be used in a secure computation revealing only …

boston-university
The community cache with complete information

Kariz is a new architecture for caching data from data-lakes accessed, potentially concurrently, by multiple analytic platforms. It integrates rich …

, boston-university northeastern-university
Say Goodbye to Off-heap Caches! On-heap Caches Using Memory-Mapped I/O

“Many analytics computations are dominated by iterative processing stages, executed until a convergence condition is met. To accelerate such workloads …

university-of-crete
Transparent Compiler and Runtime Specializations for Accelerating Managed Languages on FPGAs

“In recent years, heterogeneous computing has emerged as the vital way to increase computers’ performance and energy efficiency by combining …

university-of-manchester
You can’t hide you can’t run: a performance assessment of managed applications on a NUMA machine

The ever-growing demand for more memory capacity from applications has always been a challenging factor in computer architecture. The advent …

university-of-manchester
Real-Time Data Stream Processing

Introduction – why stream processing? It is commonly known that we are living in the era of Big Data. At …

technion
Fooling primality tests on smartcards

We analyse whether the smartcards of the JavaCard platform correctly validate primality of domain parameters.

masaryk-university
Minerva: The curse of ECDSA nonces

We present our discovery of a group of side-channel vulnerabilities in implementations of the ECDSA signature algorithm in a widely …

masaryk-university
User Testing of Mobile Banking Authentication Methods: UX Testing, User Interviews, and Quantitative Survey

This report describes the results of testing of authentication methods and applications for smartphones, including the methodology that was used. …

masaryk-university
Simulation Games Platform for Unintentional Perpetrator Attack Vector Identification

Cyber-security protection of critical systems is one of the major challenges of today. Although the attacks typically originate from attackers …

masaryk-university
Impact of methodological choices on the evaluation of student models

The evaluation of student models involves many methodological decisions, e.g., the choice of performance metric, data filtering, and cross-validation setting. Such issues may seem like technical details, and they do not get much attention in published research.

masaryk-university
Conclave: secure multi-party computation on big data (extended TR)

Secure Multi-Party Computation (MPC) allows mutually distrusting parties to run joint computations without revealing private data. Current MPC algorithms scale …

boston-university
CHIPS: A Service for Collecting, Organizing, Processing, and Sharing Medical Image Data in the Cloud

Web browsers are increasingly used as middleware platforms offering a central access point for service provision. Using backend containerization, RESTful …

boston-university
M2: Malleable Metal as a Service

Existing bare-metal cloud services that provide users with physical servers have a number of serious disadvantages over their virtual alternatives, …

, , boston-university northeastern-university
Caching in the Multiverse

To get good performance for data stored in Object storage services like S3, data analysis clusters need to cache data …

, boston-university northeastern-university
A Secure Cloud with Minimal Provider Trust

Bolted is a new architecture for a bare metal cloud with the goal of providing security-sensitive customers of a cloud …

, , boston-university northeastern-university
Supporting Security Sensitive Tenants in a Bare-Metal Cloud

SecCloud is a new architecture for bare-metal clouds that enables tenants to control tradeoffs between security, price, and performance. It …

, , boston-university northeastern-university
A fork() in the road

The received wisdom suggests that Unix’s unusual combination of fork() and exec() for process creation was an inspired design. In …

boston-university
Unikernels: The Next Stage of Linux’s Dominance

Unikernels have demonstrated enormous advantages over Linux in many important domains, causing some to propose that the days of Linux’s …

boston-university
SEUSS: Rapid serverless deployment using environment snapshots

Modern FaaS systems perform well in the case of repeat executions when function working sets stay small. However, these platforms …

, boston-university
D3N: A multi-layer cache for the rest of us

Current caching methods for improving the performance of big-data jobs assume high (e.g., full bi-section) bandwidth; however many enterprise data …

, boston-university northeastern-university
SEUSS: skip redundant paths to make serverless fast

This paper presents a system-level method for achieving the rapid deployment and high-density caching of serverless functions in a FaaS …

, boston-university
Efficient Adaptive Detection of Complex Event Patterns

Complex event processing (CEP) is widely employed to detect occurrences of predefined combinations (patterns) of events in massive data streams.

technion
Join Query Optimization Techniques for Complex Event Processing Applications

Complex event processing (CEP) is a prominent technology used in many modern applications for monitoring and tracking events of interest in massive data streams.

technion
Beyond Binary Correctness: Classification of Students’ Answers in Learning Systems

Additive Factors Model is a widely used student model, which is primarily used for refining knowledge component models (Q-matrices).

masaryk-university
Towards Non-Intrusive Software Introspection and Beyond

Continuous verification and security analysis of software systems are of paramount importance to many organizations. The state-of-the-art for such operations …

, boston-university northeastern-university
Role-Based Ecosystem for the Design, Development, and Deployment of Secure Multi-Party Data Analytics Applications

Software applications that employ secure multi-party computation (MPC) can empower individuals and organizations to benefit from privacy-preserving data analyses when …

boston-university
Tutorial: Deploying Secure Multi-Party Computation on the Web Using JIFF

Secure multi-party computation (MPC) enables joint computation over private data sets contributed by multiple entities. Using MPC in real-world software …

boston-university
Exploration of the Robustness and Generalizability of the Additive Factors Model

Additive Factors Model is a widely used student model, which is primarily used for refining knowledge component models (Q-matrices).

masaryk-university
Real-Time Multi-Pattern Detection over Event Streams

In this paper, we present a novel framework for real-timemulti-pattern complex event processing.

technion
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 …

masaryk-university
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 …

masaryk-university
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 …

masaryk-university
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 …

masaryk-university
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 …

masaryk-university
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 …

masaryk-university
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 …

masaryk-university
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 …

masaryk-university
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 …

masaryk-university
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 …

masaryk-university
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 …

masaryk-university
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. …

masaryk-university
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). …

masaryk-university
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: Pge …

masaryk-university
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 …

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

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 end users. Moreover, it is unclear how much does the content of error messages and documentation influence these perceptions.

masaryk-university
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 …

String Abstraction for Model Checking of C Programs

In this paper, we elaborate an abstract domain for C strings, that is, null-terminated arrays of characters. We describe the abstract semantics of basic string operations and prove their soundness with regards to previously established concrete semantics of those operations.

masaryk-university
Extending DIVINE with Symbolic Verification Using SMT

DIVINE is an LLVM-based verification tool focusing on anal- ysis of real-world C and C++ programs. Such programs often interact with their environment, for example via inputs from users or network. When these programs are analyzed, it is desirable that the verification tool can deal with inputs symbolically and analyze runs for all inputs. In DIVINE, it is now possible to deal with input data via symbolic computa- tion instrumented into the original program at the level of LLVM bitcode.

masaryk-university
Symbolic Computation via Program Transformation

Symbolic computation is an important approach in automated program analysis. Most state-of-the-art tools perform symbolic computation as interpreters and directly maintain symbolic data. In this paper, we show that it is feasible, and in fact practical, to use a compiler-based strategy instead.

masaryk-university