Title
HyperSSE: Static Analysis of Real-Time Hypervisor Systems

Authors
Mareike	Burg	burg@sra.uni-hannover.de	Germany	Leibniz Universität Hannover

Abstract
With performance increases in recent years, embedded systems developed from small microcontrollers towards powerful and interconnected multicore compute units. New applications demand complex interactions between a growing number of components, integrating safety-critical real-time control systems with less critical devices and sensors. This leads to the consolidation of previously independent systems onto shared hardware platforms and the development of embedded virtualization.
To maintain safety-related constraints, hypervisors statically partition and allocate hardware resources for critical systems, protecting high-priority guests from the side effects of other guests. This enables mixed criticality, where multiple guests with different real-time conditions coexist on a shared virtualization platform. To develop and verify a platform with high resource utilization, a detailed analysis of each system's behavior and interactions is required.
This talk presents the Hypervisor System State Enumeration (HyperSSE), providing a static analysis model of multiple applications and their operating systems in parallel. It extends upon the previously published MultiSSE algorithm from the Automated Real-time system Analyzer (ARA) and expands its multicore model towards a multi-operating system model, making it possible to track interaction semantics across different kinds of operating systems. This allows to analyze when in their control flow each guest uses system or hypercalls to access resources.
To evaluate the viability of this approach, a diverse array of test cases is successfully analyzed and manually verified to match the expected control flows. A Xen event channel mechanism sends notifications across AUTOSAR and Zephyr guests, finding all possible cross-system control flows and predicting possible interaction patterns using worst-case and best-case execution time estimates. An automatic test system builds and manages all guests and their applications; another example shows, with a proof-of-concept system, how to port a given analyzable system onto hardware. The HyperSSE proves the possibility of cross-operating system analysis and gives new insight into the virtualization abstraction layer.