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.
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 … This report describes the results of testing of authentication methods and applications for smartphones, including … Cyber-security protection of critical systems is one of the major challenges of today. Although the … 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 … Web browsers are increasingly used as middleware platforms offering a central access point for service … Existing bare-metal cloud services that provide users with physical servers have a number of serious … To get good performance for data stored in Object storage services like S3, data analysis … Bolted is a new architecture for a bare metal cloud with the goal of providing … SecCloud is a new architecture for bare-metal clouds that enables tenants to control tradeoffs between … The received wisdom suggests that Unix’s unusual combination of fork() and exec() for process creation … Unikernels have demonstrated enormous advantages over Linux in many important domains, causing some to propose … Modern FaaS systems perform well in the case of repeat executions when function working sets … Current caching methods for improving the performance of big-data jobs assume high (e.g., full bi-section) … This paper presents a system-level method for achieving the rapid deployment and high-density caching of … 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. … Software applications that employ secure multi-party computation (MPC) can empower individuals and organizations to benefit … Secure multi-party computation (MPC) enables joint computation over private data sets contributed by multiple entities. … 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 … In model checking of real-life C and C++ programs, both search efficiency and counterexample readability … We present a new release of the parallel and distributed LTL model checker DiVinE. The major … Model checking became a standard method of analyzing complex systems in many application domains. No … We present a new design and a C++ implementation of a high-performance, cache-efficient hash table … In this paper, we present substantial improvements in efficiency of explicit-state LTL model checking of … In this paper, we present substantial improvements in efficiency of explicit-state LTL model checking of … We present an extension of the DIVINE software model checker to support programs with exception … Abstract: The fourth version of the DIVINE model checker provides a modular platform for verification … Data races are among the most difficult software bugs to discover. They arise from multiple … Many full disk encryption applications rely on a strong password-based key derivation function to process … Full disk encryption (FDE) is a common way to prevent unauthorized use of data by … Full Disk Encryption (FDE) provides confidentiality of a data-at-rest stored on persistent devices like disk … Research cooperation of CRoCS, Faculty of Informatics, Masaryk University and Red Hat. Authors: Martin Ukrop and Vashek Matyas Conference: RSA … Many starting teachers of computer science have great professional skill but often lack pedagogical training. … 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 … 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 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