überSpark: Practical, Provable, End-to-End Guarantees on Commodity HeterogenousInterconnected Computing Platforms

überSpark is designed to be realizable on heterogeneous hardware platforms with disparate capabilities, and facilitates compositional end-to-end reasoning and efficient implementation. überSpark also supports the use of multiple verification techniques towards properties of different flavors, for development compatible, incremental verification, co-existing and meshing with unverified components, at a fine granularity, and wide applicability to all layers of the CHIC stack. We will discuss the CHIC stack challenges, illustrate our design decisions, describe the überSpark architecture, present our foundational steps, and outline on-going and future research activities. We anticipate überSpark to retrofit and unlock a wide range of unprecedented end-to-end provable guarantees on today’s continuously evolving CHIC stack.

BIO

Amit Vasudevan is a Computer Scientist at the Software Engineering Institute (SEI), Carnegie Mellon University (CMU). He received his Ph.D. and M.S degrees from the Computer Science Department at UT Arlington and spent three years as a Post-doctoral fellow at CyLab, Carnegie Mellon University. Before that, he obtained his B.E. from the Computer Science Department at the BMS College of Engineering, Bangalore, India. His research interests include secure (embedded) systems and IoT, virtualization, trusted computing, formal methods, malware analysis and operating systems (see https://hypcode.org). His present research focuses on building formally verifiable and trustworthy computing systems. He is the principal force behind the design and development of uberSpark (https://uberspark.org) – an innovative architecture and framework for compositional formal verification of security properties of commodity system software; and the uber eXtensible Micro-Hypervisor Framework (uberXMHF; https://uberxmhf.org) – an open-source, extensible and formally verifiable micro-hypervisor framework which forms the foundation for a new class of (security-oriented) micro-hypervisor based applications (“uberapps”) on commodity computing platforms. When low-level tinkering with computing platforms, IoTs, drones, and such get too much for him, he can be found spending time with his wife and kids, meditating and wood-working amidst the Texas ranches and longhorns.

Amit Vasudevan, SEI/Carnegie Mellon University (PI)
Jeff Boleng, SEI/Carnegie Mellon University (co-PI)
Bruce Krogh, SEI/Carnegie Mellon University
Anton Dimov Hristozov, SEI/Carnegie Mellon University
Ruben Martins, CSD/Carnegie Mellon University
Raffaele Romagnoli, ECE/Carnegie Mellon University