Building Verifiable and Trustworthy Computing Systems

About

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. His present research focuses on building formally verifiable and trustworthy computing systems. He is the principal force behind the design and development of uberSpark – an innovative architecture and framework for compositional formal verification of security properties of commodity system software; and the uber eXtensible Micro-Hypervisor Framework (uberXMHF) – 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.

Quests

  • amit-vasudevan-quests-2018

    2018

    System Security Researcher; SEI, Carnegie Mellon University

    Created uberPI, the first micro-hypervisor based security architecture and framework for the ubiquitous embedded computing platform, the Raspberry PI.
       
    c18 "Have your PI and Eat it Too: Practical Security on a Low-cost Ubiquitous Computing Platform. Proceedings of the IEEE European Symposium on Security and Privacy, 2018.
    [paper.pdf | paper.bib]
       
    Best Paper Award; IEEE European Symposium on Security and Privacy, 2018.
       
    Open-source release of uberPI as part of the uber eXtensible Micro-Hypervisor Framework (uberXMHF)

  • amit-vasudevan-quests-2017

    2017

    System Security Researcher; Cylab & SEI, Carnegie Mellon University

    Continued open-source development of uberSpark and the uber eXtensible Micro-Hypervisor Framework (uberXMHF)
       
    Explored the feasibility of architecting a performant micro-hypervisor based system security framework on low-cost commodity embedded platforms.

  • amit-vasudevan-quests-2016

    2016

    Research Scientist; CyLab, Carnegie Mellon University

    Created uberSpark, an innovative system architecture for compositional verification of security properties of extensible hypervisors written in low-level languages such as C and Assembly. uberSpark focuses on minimal runtime performance overheads, verified system properties ( e.g., via invariants) and commodity compatibility (enabling developers to embrace verification more readily while supporting unmodified OSes such as Linux on commodity x86 hardware platforms).
       
    c17 "uberSpark: Enforcing Verifiable Object Abstractions for Automated Compositional Security Analysis of a Hypervisor". In Proceedings of the USENIX Security Symposium, 2016
    [paper.pdf | paper.bib]
       
    Created the uber eXtensible Micro-Hypervisor Framework (uberXMHF), the successor to the eXtensible Micro-Hypervisor Framework (XMHF), which employs uberSpark to realize a compositionally verifiable micro-hypervisor framework for commodity platforms.
       
    Started the open-source development of uberSpark and the uber eXtensible Micro-Hypervisor Framework (uberXMHF)
       

  • amit-vasudevan-quests-2015

    2015

    Research Scientist; CyLab, Carnegie Mellon University

    Continued open-source development of the eXtensible Micro-Hypervisor Framework (XMHF)
       
    Continued investigation on a compositionally verfiable micro-hypervisor framework.with the following goals: system performance, verified system properties and commodity-compatibility.

  • amit-vasudevan-quests-2014

    2014

    Research Scientist; CyLab, Carnegie Mellon University

    Authored a book (by invitation) with Springer Link on Trustworthy Computing on Mobule Systems which is an extended edition of our previous conference paper.
       
    b1 "Trustworthy execution on mobile devices. What security properties can my mobile platform give me?". Springer Briefs in Computer Science. Springer, ISBN 978-1-4614-8189-8, 2014
    [book.pdf | book.bib]
       
    Continued open-source development of the eXtensible Micro-Hypervisor Framework (XMHF)
       
    Started exploring the feasibility of a compositionally verfiable micro-hypervisor framework.

  • amit-vasudevan-quests-2013

    2013

    Research Scientist; CyLab, Carnegie Mellon University

    Applied the CARMA framework along with a CPU instruction set extension for externally verifiable initiation, execution and termination of an isolated execution environment with the CPU being the sole trusted computing base.
       
    c16 "OASIS: on achieving a sanctuary for integrity and secrecy on untrusted platforms". In Proceedings of the ACM Conference on Computers and Communication Security, 2013
    [paper.pdf | paper.bib]
       
    Created the eXtensible Micro-Hypervisor Framework (XMHF), a clean, bare-bones, formally verifiable micro-hypervisor framework which forms the foundation for a new class of (security-oriented) hypervisor-based applications ("hypapps").
       
    c15 "Design, Implementation and Verification of an eXtensible and Modular Hypervisor Framework". In Proceedings of the IEEE Symposium on Security and Privacy, 2013
    [paper.pdf | paper.bib]
       
    Started the open-source development of the eXtensible Micro-Hypervisor Framework (XMHF)
       
    Created a hypervisor based system architecture for verifiable resource accounting for outsourced computations.
       
    c14 "Towards Verifiable Resource Accounting for Outsourced Computation". In Proceedings of the ACM Conference on Virtual Execution Environments, 2013
    [paper.pdf | paper.bib]
       

  • amit-vasudevan-quests-2012

    2012

    Research Scientist; CyLab, Carnegie Mellon University
    Senior Security Architect; NoFuss Inc.

    Realized secure execution trace recording on commodity Intel x86 platforms in the context of application-level binary analysis.
       
    c13 "Down to the Bare Metal: Using Processor Features for Binary Analysis". In Proceedings of the IEEE Annual Computer Security and Applications Conference, 2012
    [paper.pdf | paper.bib]
       
    Created "CARMA", a tamper resistant isolated execution environment on commodity AMD x86 platforms. CARMA leverages cache-as-ram capabilities of the CPU to create an execution environment backed by resources entirely within the CPU die.
       
    c12 "CARMA: a hardware tamper-resistant isolated execution environment on commodity x86 platforms". In Proceedings of the ACM Asia Conference on Computer and Communications Security, 2012
    [paper.pdf | paper.bib]
       
    Formally verified shadow page-table implementation of a special purpose hypervisor on commodity Intel x86 platforms.
       
    c11 "Parametric Verification of Address Space Separation". In Proceedings of the International Conference on Principles of Security and Trust, 2012
    [paper.pdf | paper.bib]
       
    Created a special-purpose hypervisor called "Lockdown" to achieve practical "red-green" system split on commodity x86 platforms running both Windows and Linux OSes towards security applications.
       
    c10 "Lockdown: Towards a Safe and Practical Architecture for Security Applications on Commodity Platforms". In Proceedings of the Internaltional Conference on Trust and Trustworthy Computing, 2012
    [paper.pdf | paper.bib]
       
    Compiled the first of a kind systematic analysis and report on realizing practical and deployable security on mobile devices.
       
    c9 "Trustworthy Execution on Mobile Devices: What Security Properties Can My Mobile Platform Give Me?". In Proceedings of the International Conference on Trust and Trustworthy Computing, 2012
    [paper.pdf | paper.bib]
       
    Started exploring the feasibility of automated formal verification of a micro-hypervisor on commodity platforms.

  • amit-vasudevan-quests-2011

    2011

    Research Scientist; CyLab, Carnegie Mellon University
    Senior Security Architect; NoFuss Inc.

    Created a system-wide, real-time, trustworthy instruction execution tracing framework on commodity AMD x86 platforms. The framework, codenamed XTRec leverages a debugging feature called branch trace messaging in conjunction with a special-purpise hypervisor to securely log instruction traces during runtime.
       
    c8 "XTRec: Secure Real-Time Execution Trace Recording on Commodity Platforms". In Proceedings of the Hawaii International Conference on System Sciences, 2011
    [paper.pdf | paper.bib]
       
    Began investigating tamper resistant isolated execution environments on commodity x86 platforms.
       
    Started exploring the feasibility of a practical "red-green" split execution on commodity OSes and hardware platforms.

  • amit-vasudevan-quests-2010

    2010

    Research Scientist; CyLab, Carnegie Mellon University
    Senior Security Architect; NoFuss Inc.

    Compiled a first of a kind system level analysis and requirements for an integrity protected hypervisor on the x86 hardware virtualized architecture.
       
    c7 "Requirements for an Integrity-Protected Hypervisor on the x86 Hardware Virtualized Architecture".In Proceedings of the International Conference on Trust and Trustworthy Computing, 2010
    [paper.pdf | paper.bib]
       
    Continued exploration of system level trustworthy execution tracing on commodity x86 platforms leveraging a special-purpise hypervisor.

  • amit-vasudevan-quests-2009

    2009

    Post-doctoral Fellow; CyLab, Carnegie Mellon University

    Created a more robust stealth breakpoint framework geared towards analysis of BIOS andfirmware level malware.
       
    c6 "Re-inforced stealth breakpoints". In Proceedings of the IEEE Conference on Risks and Security of Internet and Systems, 2009
    [paper.pdf | paper.bib]
       
    Started exploration on the design space of system level trustworthy execution tracing on commodity x86 platforms.

  • amit-vasudevan-quests-2008

    2008

    Post-doctoral Fellow; CyLab, Carnegie Mellon University

    Created an OS level framework to detect and remove 0-day malware without relying on signatures or heuristics. The framework was a result of exploring a design space that was heavily inspired by a "git" like revision control system to maintain multiple (revertible) critical OS state during runtime.
       
    c5 "MalTRAK: Tracking and Eliminating Unknown Malware". In Proceedings of the Annual Computer Security and Applications Conference, 2008
    [paper.pdf | paper.bib]
       
    Explored the design, implementation and evaluation of a special purpose hypervisor towards protecting kernel root-kits on Intel x86 hardware-virtualized platforms.

  • amit-vasudevan-quests-2004-2007

    2004 - 2007

    Doctor of Philosopy in Computer Science and Engineering, University of Texas at Arlington
     [GPA: 4.0/4.0]

    Wrote and defended my dissertation on an integrated stealth runtime binary analysis framework for dynamic malware analysis.
    [thesis.pdf | thesis.bib]
       
    University Scholar Award (Twice)
       
    Outstanding Teaching Award
       
    c4 "SPiKE: Engineering malware analysis tools using unobtrusive binary-instrumentation". In Proceedings of the Australasian Computer Science Conference, 2006.
    [paper.pdf | paper.bib]
       
    c3 "Cobra: Fine-grained Malware Analysis using Stealth Localized-executions".In Proceedings of the IEEE Symposium on Security and Privacy, 2006
    [paper.pdf | paper.bib]
       
    c2 "Stealth Breakpoints". In Proceedings of the Annual Computer Security and Applications Conference, 2005
    [paper.pdf | paper.bib]
       
    c1 "A High Performance Kernel-Less Operating System Architecture". In Proceedings of the Australasian Computer Science Conference, 2005
    [paper.pdf | paper.bib]

  • amit-vasudevan-quests-2002-2003

    2002 - 2003

    Masters of Computer Science and Engineering, University of Texas at Arlington
     [GPA: 4.0/4.0]

    Wrote and defended my Masters thesis on a multi-architecture dynamic binary instrumentation framework for commodity operating systems.
    [thesis.pdf | thesis.bib]
       
    Masters Dean Fellowship Award
       
    Explored the design, implementation and evaluation of a dynamic binary instrumentation framework for commodity OSes supporting multiple CPU architectures.

  • amit-vasudevan-quests-1997-2001

    1997 - 2001

    Bachelors of Computer Science and Engineering, BMS College of Engineering, India
     [GPA: 3.9/4.0]

  • hypcode