Biblio

Remote Attestation ( RA) is a security service that enables a trusted verifier ( Vrf) to measure current memory state of an untrusted remote prover ( Prv). If correctly implemented, RA allows Vrf to remotely detect if Prv's memory reflects a compromised state. However, RA by itself offers no means of remedying the situation once P rv is determined to be compromised. In this work we show how a secure RA architecture can be extended to enable important and useful security services for low-end embedded devices. In particular, we extend the formally verified RA architecture, VRASED, to implement provably secure software update, erasure, and system-wide resets. When (serially) composed, these features guarantee to Vrf that a remote Prv has been updated to a functional and malware-free state, and was properly initialized after such process. These services are provably secure against an adversary (represented by malware) that compromises Prv and exerts full control of its software state. Our results demonstrate that such services incur minimal additional overhead (0.4% extra hardware footprint, and 100-s milliseconds to generate combined proofs of update, erasure, and reset), making them practical even for the lowest-end embedded devices, e.g., those based on MSP430 or AVR ATMega micro-controller units (MCUs). All changes introduced by our new services to VRASED trusted components are also formally verified.

In 1999, Micali, Rabin and Vadhan introduced the notion of Verifiable Random Functions (VRF)$\backslash$citeFOCS:MicRabVad99. VRFs compute for a given input x and a secret key \$sk\$ a unique function value \$y=V\_sk (x)\$, and additionally a publicly verifiable proof $π$. Each owner of the corresponding public key \$pk\$ can use the proof to non-interactivly verify that the function value was computed correctly. Furthermore, the function value provides the property of pseudorandomness. Most constructions in the past are based on q-type assumptions. Since these assumptions get stronger for a larger factor q, it is desirable to show the existence of VRFs under static or general assumptions. In this work we will show for the constructions presented in $\backslash$citePKC:DodYam05 $\backslash$citeCCS:BonMonRag10 the equivalence of breaking the VRF and solving the underlying q-type assumption.

Accurate, precise, and unambiguous definitions of software weaknesses (bugs) and clear descriptions of software vulnerabilities are vital for building the foundations of cybersecurity. The Bugs Framework (BF) comprises rigorous definitions and (static) attributes of bug classes, along with their related dynamic properties, such as proximate, secondary and tertiary causes, consequences, and sites. This paper presents an overview of previously developed BF classes and the new cryptography related classes: Encryption Bugs (ENC), Verification Bugs (VRF), and Key Management Bugs (KMN). We analyze corresponding vulnerabilities and provide their clear descriptions by applying the BF taxonomy. We also discuss the lessons learned and share our plans for expanding BF.