About Research Day Europe 2020
On January 23rd, the day before DevConf.cz, Red Hat Research held its first annual Research Day Europe in Brno at the freshly renovated Hotel Passage.
Research Day brought together an audience of about 130 invited participants from academia, Red Hat customers, Red Hat partners, and also companies interested in research and cooperation with universities to exchange ideas, share their experiences, achievements and common passion for open source research.
Research Day featured researchers from around the world presenting current research projects such as encryption, crypto-algorithms, new forms of attacks, and work on automation of formal code verification.
Research Day Europe Themes and Topics
The first European Research Day covered following themes that show how academic research projects are addressing critical issues:
- Data-Intensive Science and Software
- Security and privacy
- Code analysis and verification
Based on these topics the program was divided into 3 tracks featuring
19 speakers from Red Hat and academic circles, namely from universities in Czech Republic, Graz (Austria), Leuven (Belgium), Newcastle and Birmingham (UK), and Massachusetts in the US.
Research Day Europe Agenda
Track: Data-Intensive Science and Software
9:00am – 9:30am
Open Cloud Testbed Developing a Testbed for the Research Community Exploring Next-Generation Cloud Platforms
By Michael Zink, University of Massachusetts Amherst
Show the abstract
Cloud testbeds are critical for enabling research into new cloud technologies – research that requires experiments that potentially change the operation of the cloud itself. Several such testbeds have been created in the recent past (e.g., Chameleon, CloudLab, etc.) with the goal to support the CISE systems research community. It has been shown that these testbeds are very popular and heavily used by the research community. Testbed utilization often reaches 100%, especially ahead of deadlines for major systems conferences, while there are also periods of modest (<40%) testbed usage.
In my talk, I will present our NSF “Open Cloud Testbed” (OCT) project, which has the goal to enable elastic cloud testbeds for systems research. Eventually, OCT will allow cloud testbeds to grow and shrink by allocating and deallocating additional resources from compute facilities like production clouds and HPC clusters. Within the OCT project, we will create a prototype elastic cloud testbed, which will combine proven software technologies from both the CloudLab and the Massachusetts Open Cloud (MOC) projects. It will also combine a research cloud testbed (CloudLab) with a production cloud (MOC) through OCT’s tight integration with the latter and federation with CloudLab. In addition, OCT will provide programmable hardware (FPGAs) as Bump-in-the-Wire (BITW) capabilities not present in other facilities available to researchers today. The combination of a testbed and production cloud allows a) larger scale compared to isolated testbeds, b) reproducible experimentation based on realistic user behavior and applications, as well as c) a model for transitioning successful research results to practice. OCT offers a unique sustainability model, by allowing additional compute resources to be dynamically moved from institutional uses into the testbed and back again, providing a path to growth beyond the initial testbed.
9:30am – 10:00am
Machine Learning for Adaptive Human Learning
By Radek Pelánek, Masaryk University
Show the abstract
Our Adaptive Learning Group (Faculty of Informatics, MU Brno) has developed adaptive educational systems for several domains (e.g., programming, mathematics, grammar, geography). I will provide an overview of our systems and discuss machine learning techniques that we use to improve the learning of our (human) users. I will also provide examples of our research, which often deals with methodological issues in the evaluation of machine learning techniques that are relevant beyond the development of educational applications.
10:00am – 10:30am
Acoustic Identification of Cetaceans
By Georgia Atkinson, Newcastle University
Show the abstract
Modelling cetacean (dolphins, whales and porpoises) population dynamics is paramount for effective conservation and population management. Methodologies for cetacean research include passive acoustic monitoring (PAM) which allows for monitoring of cetacean occurrence and behaviour ecology through underwater recording. Due to high volumes of data collected and stored in PAM systems, there is a need for automated solutions that can detect and classify cetacean vocalisations. In this talk, we shall discuss how signal processing and deep learning techniques can be applied to this problem and see initial results for detection.
10:30am – 11:00am
Automating Computational Placement in IoT Environments
By Peter Michalák, Newcastle University
Show the abstract
The suitability of high-level declarative language use for automatic generation of run-time infrastructure with a range of non-functional requirements placed on Internet of Things environments – notably Energy and Bandwidth – will be discussed in the talk. This unique perspective allows domain experts to distribute computation over IoT devices, field gateways, and clouds with little programming knowledge. An overview of the proposed PATH2iot open source platform will be presented – walking the audience through optimisation techniques to make offloading decisions taking into consideration the current state of infrastructure, description of computation and set of non-functional requirements, as well as the automated deployment process. Significant improvements to deployment plans for two real- world use cases have been achieved: a healthcare application resulted in substantial battery savings of a wearable device; and a smart city use case designed for real- time audio signal analytics to detect train arrivals, where the optimised deployment plan satisfied strict bandwidth constraints imposed by LoRaWAN technology.
11:00am – 11:30am
OpenShift-based High-Performance Computing for Research in Astrophysics
By Filip Hubík, Red Hat; Nikolaos Moraitis, Red Hat; Gabriel Szász Masaryk University & Zdeněk Švécar, Red Hat
Show the abstract
Our curiosity is constantly pushing technology towards higher goals, unveiling the secrets of distant realms far beyond our imagination.
Masaryk University, in collaboration with the Brno Red Hat office, initiated an ambitious project that has the potential to redefine what we have known about the stars in our Local Universe. Powerful open source tools, especially the Red Hat OpenShift Container Platform, are making this extensive project feasible.
In this talk you will hear from four presenters: a Project Manager, a Graduate Student in Astrophysics, and two Red Hat Developers, all working together on a new approach involving stellar rotation as an essential parameter while focusing on reproducibility, parallelization and simplicity.
11:30am – 12:00pm
Avoiding bad Decisions and Heuristics
By Ulrich Drepper, Red Hat
Show the abstract
In many software projects and especially in system software programmers have incomplete knowledge about the actual use cases. To provide the needed flexibility, performance, etc. these software projects often feature many, too many, configuration options. Some are exposed to the user, some internally controlled by heuristics. Unless both the developer and the user spend a huge amount of time tuning, the resulting system will not run optimally. Additionally, settings are then often applied statically while the environment constantly changes due to new software version, new hardware, or changing workloads.
One way out is to have the system learn about the best settings. If this happens for each deployment the solution could be locally optimal and adding more flexibility in the implementation can lead to better performance and not just higher complexity.
The compiler is a piece of system software that has several heuristics built in. In this talk Uli will go over the problem statement and using the example of the compiler describe ways to achieve self-tuning system using machine learning. These are not solved problems and a goal of the talk is to get researchers interested in tackling these problems together with Red Hat.
Track: Security and Privacy
1:00pm – 1:30pm
Observing developers interacting with TLS certificates
By Martin Ukrop, Masaryk University
Show the abstract
Over the past three years, we have conducted several experiments observing IT professionals interacting with TLS certificates. The two most prominent of these experiments took place at DevConf.CZ 2017 and DevConf.CZ 2018. We investigated the usability of OpenSSL (as of 2019, the most common library for manipulating X.509 certificates), the developers’ understanding of multiple certificate issues and the trust they have to such flawed certificates. Conclusions based on these observations can help us produce an environment that is more usable for IT professionals resulting in fewer vulnerabilities in developed products.
.
1:30pm – 2:00pm
Analyzing, breaking and improving certified cryptographic hardware (TPMs and smartcards)
By Petr Švenda, Masaryk University
Show the abstract
Cryptographic hardware like smartcards or Trusted Platform Modules (TPMs) is a crucial component of many security systems, serving as an authentication token, digital signature device, secure storage for encryption keys, or providing a platform’s root of trust. Despite the existence of extensive security certification schemes like Common Criteria or NIST FIPS140-2, the security vulnerabilities are still found in such devices, partially due to the overall closeness of the secure hardware ecosystem.
The talk will present a suite of the open tools for black-box security analysis of cryptographic hardware developed by CRoCS laboratory at Masaryk University, and vulnerabilities found like ROCA (CVE-2017-15361) or Minerva (CVE-2019- 15809) which lead to large practical impact with estimated 1-2 billion devices affected worldwide.
2:00pm – 2:30pm
Improving disk encryption in Linux
By Milan Brož, Red Hat | Masaryk University
Show the abstract
Disk Encryption has become a widely used security feature used in all types of data processing systems today – from mobile devices up to large cloud systems. This talk is an overview of several recent improvements in Linux disk encryption like data integrity protection based on authenticated encryption or using memory- hard key derivation for protection of disk unlocking passphrases. It demonstrates that an applied research collaboration between a university research laboratory and upstream developers can produce not only academic publications but also new features in open source projects.
2:30pm – 3:00pm
Leaky processors: Lessons from Spectre, Meltdown, and Foreshadow
By Jo Van Bulck, The Katholieke Univeriteit Leuven & Daniel Gruss, Graz University of Technology
Show the abstract
Over the past decades, security has been largely regarded as a software developer’s responsibility, while hardware vendors have focused on making processors faster. However, now that security researchers are exploring ever- deeper parts of the system stack, it has been shown that these impressive performance improvements also come with a cost. With the announcement of the Spectre, Meltdown, and Foreshadow CPU vulnerabilities in 2018, an entirely new and dangerous class of transient execution attacks has arisen. Crucially, these attacks cross the hardware-software boundary, thereby challenging decades of performance gains and ultimately eradicating the viewpoint of security as an exclusive software responsibility. This talk will review transient-execution processor vulnerabilities from the ground up. We will discuss Spectre, Meltdown, Foreshadow, and more recent variants. Finally, the talk will discuss the long-term insights behind this recent wave of attacks, as well as mitigation strategies across the application, compiler, operating system, and CPU microcode levels.
3:00pm – 3:30pm
Plundervolt: Pillaging and plundering SGX with Software-based Fault Injection Attacks
By Kit Murdock, the University of Birmingham
Show the abstract
Many modern processors expose privileged software interfaces to dynamically modify the frequency and voltage. These interfaces were introduced to cope with the ever-growing power consumption of modern computers. In this talk we show how these privileged interfaces can be exploited to undermine the system’s security. We present the Plundervolt attack – demonstrating how we can corrupt the integrity of Intel SGX computations.
Track: Code Analysis and Verification
4:00pm – 4:20pm
Formal Verification of a Linux Distribution (Automated Formal Verification)
By Kamil Dudka, Red Hat
Show the abstract
Red Hat uses static analyzers to automatically find bugs in the source code of Red Hat Enterprise Linux, consisting of approx. 3000 RPM packages and 300 million lines of code. There are open source tools that can statically analyze this amount of software in a fully automatic way. Would it be possible to use formal verification tools to find bugs in (or even prove the correctness of) the important pieces of code in our Linux distribution? Red Hat is now experimenting with formal verifiers Symbiotic and Divine, which are developed by research groups of Masaryk University in Brno.
Are these tools ready for industrial software? How much are we able to integrate them into our release pipeline?
4:20pm – 4:40pm
Symbiotic: program slicing framework (Automated Formal Verification)
By Marek Chalupa, Masaryk University
Show the abstract
Symbiotic is a framework that takes a C or LLVM program and generates a new program suited to analysis and verification. To reach its aims, Symbiotic uses instrumentation combined with static analyses, program slicing and compiler optimizations. It can also seamlessly run several program analysis tools on the generated program. In this talk, I will briefly describe how Symbiotic works and how it can be used.
4:40pm – 5:00pm
Heavy-Duty Program Analysis with DIVINE (Automated Formal Verification)
By Vladimír Štill, Masaryk University
Show the abstract
DIVINE is a tool for analysis of programs written in C and C++ that primarily targets hard-to-find bugs, including concurrency-related bugs, assertion violations, and memory errors. It is developed in the Parallel and Distributed Systems Laboratory at the Faculty of Informatics, Masaryk University. One of the main strengths of DIVINE is that it is precise and can discover bugs which are hard or impossible to find by other means. Unsurprisingly, this precision comes at some cost in the human and computing effort put to the analysis. In this presentation, we outline some of the strengths and weaknesses of DIVINE. We describe how we can use DIVINE for the analysis of programs which have source code and tests available, and what can we do if that is not the case. We also show how DIVINE can be used with programs that run in the POSIX environment, i.e., use system calls and interact with other programs using the filesystem or network. Finally, we present how we can apply DIVINE to the discovery of sporadically occurring concurrency bugs.
5:00pm – 5:30pm
Performance Versioning System
By Tomáš Fiedor, Brno University of Technology
Show the abstract
Long-term management of the performance or the resource consumption of any programming project is, indeed, a tiresome job. As a consequence, many projects are needlesly slow and deplete a computer’s precious resources. Yet, so far, there has been no effective solution! This talk introduces Perun: a tool suite, which aims at helping developers track the performance history of their projects. Perun serves as a wrapper over existing repositories and offers a suite of performance collectors and analysers. The talk will provide a brief overview of Perun’s main features and introduce selected novel techniques for, e.g. automatic detection of performance changes, generating inputs leading to bad performance, or effective modeling of the program performance.
5:30pm – 6:00pm
Efficient Runtime Verification for the Linux Kernel
By Daniel Bristot de Oliveira, Red Hat | Scuola Superiore Sant’Anna
Show the abstract
Formal verification of the Linux kernel has been receiving increasing attention in recent years, with the development of many models, from memory subsystems to the synchronization primitives of the real-time kernel. The effort in developing formal verification methods is justified considering the large code-base, the complexity in synchronization required in a monolithic kernel and the support for multiple architectures, along with the usage of Linux on critical systems, from high-frequency trading to self-driven cars. Despite recent developments in the area, none of the proposed approaches are suitable and flexible enough to be applied in an efficient way to a running kernel. Aiming to fill such a gap, this research proposes a formal verification approach for the Linux kernel, based on automata models. It presents a method to auto generate verification code from an automaton, which can be integrated into a module and dynamically added into the kernel for efficient on-the-fly verification of the system, using in-kernel tracing features. Finally, a set of experiments demonstrates verification of three models, along with performance analysis of the impact of the verification, in terms of latency and throughput of the system, showing the efficiency of the approach.