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.
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.
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 cameras and easy-to-use editing software, images can be remixed (i.e., redacted, edited, and recombined with other content) on-the-fly and...
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 road to build confidence on the temporal behavior of co-running applications has presented...
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. On the internet, images are no longer static; they have become dynamic content. Thanks to the availability of smartphones with … The proliferation of multi-core, accelerator-enabled embedded systems has introduced new opportunities to consolidate real-time systems of increasing complexity. But the … FPGAs have typically achieved high speedups for 3D Fast Fourier Transforms (FFTs) due to the presence of hard floating point … Improved support for OpenCL has been an important step towards the mainstream adoption of FPGAs as compute resources. Current research … FPGAs have been demonstrated to be capable of very high performance, especially power-performance, but generally at the cost of hand-tuned … As modern Data Center workloads become increasingly complex, constrained, and critical, mainstream CPU-centric computing has had ever more difficulty in … Multi-Party Computation (MPC) is a technique enabling data from several sources to be used in a secure computation revealing only … Kariz is a new architecture for caching data from data-lakes accessed, potentially concurrently, by multiple analytic platforms. It integrates rich … “Many analytics computations are dominated by iterative processing stages, executed until a convergence condition is met. To accelerate such workloads … “In recent years, heterogeneous computing has emerged as the vital way to increase computers’ performance and energy efficiency by combining … The ever-growing demand for more memory capacity from applications has always been a challenging factor in computer architecture. The advent … Introduction – why stream processing? It is commonly known that we are living in the era of Big Data. At … We analyse whether the smartcards of the JavaCard platform correctly validate primality of domain parameters. We present our discovery of a group of side-channel vulnerabilities in implementations of the ECDSA signature algorithm in a widely … This report describes the results of testing of authentication methods and applications for smartphones, including the methodology that was used. … Cyber-security protection of critical systems is one of the major challenges of today. Although the attacks typically originate from attackers … 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. Secure Multi-Party Computation (MPC) allows mutually distrusting parties to run joint computations without revealing private data. Current MPC algorithms scale … Web browsers are increasingly used as middleware platforms offering a central access point for service provision. Using backend containerization, RESTful … Existing bare-metal cloud services that provide users with physical servers have a number of serious disadvantages over their virtual alternatives, … To get good performance for data stored in Object storage services like S3, data analysis clusters need to cache data … Bolted is a new architecture for a bare metal cloud with the goal of providing security-sensitive customers of a cloud … SecCloud is a new architecture for bare-metal clouds that enables tenants to control tradeoffs between security, price, and performance. It … The received wisdom suggests that Unix’s unusual combination of fork() and exec() for process creation was an inspired design. In … Unikernels have demonstrated enormous advantages over Linux in many important domains, causing some to propose that the days of Linux’s … Modern FaaS systems perform well in the case of repeat executions when function working sets stay small. However, these platforms … Current caching methods for improving the performance of big-data jobs assume high (e.g., full bi-section) bandwidth; however many enterprise data … This paper presents a system-level method for achieving the rapid deployment and high-density caching of serverless functions in a FaaS … Complex event processing (CEP) is widely employed to detect occurrences of predefined combinations (patterns) of events in massive data streams. Complex event processing (CEP) is a prominent technology used in many modern applications for monitoring and tracking events of interest in massive data streams. Additive Factors Model is a widely used student model, which is primarily used for refining knowledge component models (Q-matrices). Continuous verification and security analysis of software systems are of paramount importance to many organizations. The state-of-the-art for such operations … Software applications that employ secure multi-party computation (MPC) can empower individuals and organizations to benefit from privacy-preserving data analyses when … Secure multi-party computation (MPC) enables joint computation over private data sets contributed by multiple entities. Using MPC in real-world software … Additive Factors Model is a widely used student model, which is primarily used for refining knowledge component models (Q-matrices). In this paper, we present a novel framework for real-timemulti-pattern complex event processing. An important step toward adoption of formal methods in software development is support for mainstream programming languages. Unfortunately, these languages … In model checking of real-life C and C++ programs, both search efficiency and counterexample readability are very important. In this … We present a new release of the parallel and distributed LTL model checker DiVinE. The major improvement in this new release … Model checking became a standard method of analyzing complex systems in many application domains. No doubt, a number of applications … We present a new design and a C++ implementation of a high-performance, cache-efficient hash table suitable for use in implementation … In this paper, we present substantial improvements in efficiency of explicit-state LTL model checking of C & C++ programs, building … In this paper, we present substantial improvements in efficiency of explicit-state LTL model checking of C & C++ programs, building … We present an extension of the DIVINE software model checker to support programs with exception handling. The extension consists of … Abstract: The fourth version of the DIVINE model checker provides a modular platform for verification of real-world programs. It is … Data races are among the most difficult software bugs to discover. They arise from multiple threads accessing the same memory … Many full disk encryption applications rely on a strong password-based key derivation function to process a passphrase. This article defines … Full disk encryption (FDE) is a common way to prevent unauthorized use of data by encrypting the whole storage device. … Full Disk Encryption (FDE) provides confidentiality of a data-at-rest stored on persistent devices like disk or solid state drives (SSD). … 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 … Many starting teachers of computer science have great professional skill but often lack pedagogical training. Since providing expert mentorship directly … 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. Programmable packet processing is increasingly implemented using kernel bypass techniques, where a userspace application takes complete control of the networking … 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. 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. 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. Publication Summary Universities Collaborations Institutes partner_university_hfilter Design and Analysis of Microworlds and Puzzles for Block-Based Programming Masaryk University masaryk-university Motif Mining: Finding and Summarizing Remixed Image Content University of Notre Dame KROC Institute for International Peace Studies university-of-notre-dame E-WarP: A System-wide Framework for Memory Bandwidth Profiling and Management Boston University Red Hat Collaboratory At Boston University boston-university FPGA HPC using OpenCL: Case Study in 3D FFT Boston University Red Hat Collaboratory At Boston University boston-university Unlocking Performance-Programmability by Penetrating the Intel FPGA OpenCL Toolflow Boston University Red Hat Collaboratory At Boston University boston-university An Empirically Guided Optimization Framework for FPGA OpenCL Boston University Red Hat Collaboratory At Boston University boston-university Towards Hardware as a Reconfigurable, Elastic, and Specialized Service Boston University Red Hat Collaboratory At Boston University boston-university Secret Sharing MPC on FPGAs in the Datacenter Boston University Red Hat Collaboratory At Boston University boston-university The community cache with complete information Boston University, Northeastern University Mass Open Cloud boston-university northeastern-university Say Goodbye to Off-heap Caches! On-heap Caches Using Memory-Mapped I/O University of Crete university-of-crete Transparent Compiler and Runtime Specializations for Accelerating Managed Languages on FPGAs University of Manchester university-of-manchester You can’t hide you can’t run: a performance assessment of managed applications on a NUMA machine University of Manchester university-of-manchester Real-Time Data Stream Processing Technion technion Fooling primality tests on smartcards Masaryk University CROCS masaryk-university Minerva: The curse of ECDSA nonces Masaryk University CROCS masaryk-university User Testing of Mobile Banking Authentication Methods: UX Testing, User Interviews, and Quantitative Survey Masaryk University CROCS masaryk-university Simulation Games Platform for Unintentional Perpetrator Attack Vector Identification Masaryk University masaryk-university Impact of methodological choices on the evaluation of student models Masaryk University masaryk-university Conclave: secure multi-party computation on big data (extended TR) Boston University Mass Open Cloud boston-university CHIPS: A Service for Collecting, Organizing, Processing, and Sharing Medical Image Data in the Cloud Boston University Red Hat Collaboratory At Boston University Hariri Institute for Computing boston-university M2: Malleable Metal as a Service Boston University, Northeastern University Mass Open Cloud, Red Hat Collaboratory At Boston University Hariri Institute for Computing boston-university northeastern-university Caching in the Multiverse Boston University, Northeastern University Red Hat Collaboratory At Boston University Hariri Institute for Computing boston-university northeastern-university A Secure Cloud with Minimal Provider Trust Boston University, Northeastern University Mass Open Cloud, Red Hat Collaboratory At Boston University Hariri Institute for Computing boston-university northeastern-university Supporting Security Sensitive Tenants in a Bare-Metal Cloud Boston University, Northeastern University Mass Open Cloud, Red Hat Collaboratory At Boston University Hariri Institute for Computing boston-university northeastern-university A fork() in the road Boston University Red Hat Collaboratory At Boston University Hariri Institute for Computing boston-university Unikernels: The Next Stage of Linux’s Dominance Boston University Red Hat Collaboratory At Boston University Hariri Institute for Computing boston-university SEUSS: Rapid serverless deployment using environment snapshots Boston University Mass Open Cloud, Red Hat Collaboratory At Boston University Hariri Institute for Computing boston-university D3N: A multi-layer cache for the rest of us Boston University, Northeastern University Red Hat Collaboratory At Boston University Hariri Institute for Computing boston-university northeastern-university SEUSS: skip redundant paths to make serverless fast Boston University Mass Open Cloud, Red Hat Collaboratory At Boston University Hariri Institute for Computing boston-university Efficient Adaptive Detection of Complex Event Patterns Technion technion Join Query Optimization Techniques for Complex Event Processing Applications Technion technion Beyond Binary Correctness: Classification of Students’ Answers in Learning Systems Masaryk University masaryk-university Towards Non-Intrusive Software Introspection and Beyond Boston University, Northeastern University Mass Open Cloud boston-university northeastern-university Role-Based Ecosystem for the Design, Development, and Deployment of Secure Multi-Party Data Analytics Applications Boston University Red Hat Collaboratory At Boston University Hariri Institute for Computing boston-university Tutorial: Deploying Secure Multi-Party Computation on the Web Using JIFF Boston University Red Hat Collaboratory At Boston University Hariri Institute for Computing boston-university Exploration of the Robustness and Generalizability of the Additive Factors Model Masaryk University masaryk-university Real-Time Multi-Pattern Detection over Event Streams Technion technion Using Off-the-Shelf Exception Support Components in C++ Verification Masaryk University masaryk-university Context-Switch-Directed Verification in DIVINE Masaryk University masaryk-university DiVinE 3.0 – An Explicit-State Model Checker for Multithreaded C & C++ Programs Masaryk University masaryk-university DiVinE: Parallel Distributed Model Checker Masaryk University masaryk-university Fast, Dynamically-Sized Concurrent Hash Table Masaryk University masaryk-university Improved State Space Reductions for LTL Model Checking of C & C++ Programs Masaryk University masaryk-university Improved State Space Reductions for LTL Model Checking of C & C++ Programs Masaryk University masaryk-university Model Checking C++ with Exceptions Masaryk University masaryk-university Model Checking of C and C++ with DIVINE 4 Masaryk University masaryk-university Weak Memory Models as LLVM-to-LLVM Transformations Masaryk University masaryk-university Selecting a New Key Derivation Function for Disk Encryption Masaryk University masaryk-university The TrueCrypt On-Disk Format—An Independent View Masaryk University masaryk-university Extending Full Disk Encryption for the Future Masaryk University masaryk-university Why Johnny the Developer Can’t Work with Public Key Certificates Masaryk University CROCS masaryk-university Reflective Diary for Professional Development of Novice Teachers Masaryk University masaryk-university Will You Trust This TLS Certificate? Perceptions of People Working in IT Masaryk University CROCS masaryk-university The eXpress Data Path: Fast Programmable Packet Processing in the Operating System Kernel String Abstraction for Model Checking of C Programs Masaryk University masaryk-university Extending DIVINE with Symbolic Verification Using SMT Masaryk University masaryk-university Symbolic Computation via Program Transformation Masaryk University masaryk-university