Widespread adoption and growing popularity of embedded/IoT/CPS devices make them attractive attack targets. On low-to-mid-range devices, security features are typically few or none due to various constraints. Such devices are thus subject to malware-based compromise. One popular defensive measure is Remote Attestation$(\mathcal{R}\mathrm{A})$which allows a trusted entity to determine the current software integrity of an untrusted remote device. For higher-end devices,$\mathcal{R}\mathrm{A}$is achievable via secure hardware components. For low-end (bare metal) devices, minimalistic hybrid (hardware/-software)$\mathcal{R}\mathrm{A}$is effective, which incurs some hardware modifications. That leaves certain mid-range devices (e.g., ARM Cortex-A family) equipped with standard hardware components, e.g., a memory management unit (MMU) and perhaps a secure boot facility. In this space, seL4 (a verified microkernel with guaranteed process isolation) is a promising platform for attaining$\mathcal{R}\mathrm{A}$. HYDRA [1] made a first step towards this, albeit without achieving any verifiability or provable guarantees. This paper picks up where HYDRA left off by constructing a$\mathcal{P}\text{ARseL}$architecture, that separates all user-dependent components from the TCB. This leads to much stronger isolation guarantees, based on seL4 alone, and facilitates formal verification. In$\mathcal{P}\text{ARseL}$, We use formal verification to obtain several security properties for the isolated$\mathcal{R}\mathrm{A}$TCB, including: memory safety, functional correctness, and secret independence. We implement$\mathcal{P}\text{ARseL}$in$F^{\ast}$and specify/prove expected properties using Hoare logic. Next, we automatically translate the$F^{\ast}$implementation to C using KaRaM eL, which preserves verified properties of$\mathcal{P}\text{ARseL}$, C implementation (atop seL4). Finally, we instantiate and evaluate$\mathcal{P}\text{ARseL}$on a commodity platform - a SabreLite embedded device.

Exciting recent advances in genome sequencing, coupled with greatly reduced storage and computation costs, make genomic testing increasingly accessible to individuals. Already today, one’s digitized DNA can be easily obtained from a sequencing lab and later used to conduct numerous tests by engaging with a testing facility. Due to the inherent sensitivity of genetic material and the often-proprietary nature of genomic tests, privacy is a natural and crucial issue. While genomic privacy received a great deal of attention within and outside the research community, genomic security has not been sufficiently studied. This is surprising since the usage of fake or altered genomes can have grave consequences, such as erroneous drug prescriptions and genetic test outcomes. Unfortunately, in the genomic domain, privacy and security (as often happens) are at odds with each other. In this article, we attempt to reconcile security with privacy in genomic testing by designing a novel technique for a secure and private genomic range query protocol between a genomic testing facility and an individual user. The proposed technique ensures authenticity and completeness of user-supplied genomic material while maintaining its privacy by releasing only the minimum thereof. To confirm its broad usability, we show how to apply the proposed technique to a previously proposed genomic private substring matching protocol. Experiments show that the proposed technique offers good performance and is quite practical. Furthermore, we generalize the genomic range query problem to sparse integer sets and discuss potential use cases.

With the growing popularity of the Internet-of-Things (IoT), massive numbers of specialized devices are deployed worldwide, in many everyday settings, including homes, offices, vehicles, public spaces, and factories. Such devices usually perform sensing and/or actuation. Many of them handle sensitive and personal data. If left unprotected, ambient sensing (e.g., of temperature, motion, audio, or video) can leak very private information. At the same time, some IoT devices use low-end computing platforms with few (or no) security features.There are many well-known techniques to secure sensed data, e.g., by authenticating communication end-points, encrypting data before transmission, and obfuscating traffic patterns. Such techniques protect sensed data from external adversaries, while assuming that the sensing device itself is secure. Meanwhile, both the scale and frequency of IoT-focused attacks are growing. This prompts a natural question: how to protect sensed data even if all software on the device is compromised? Ideally, in order to achieve this, sensed data must be protected from its genesis, i.e., from the time when a physical analog quantity is converted into its digital counterpart and becomes accessible to software. We refer to this property as PfB: Privacy-from-Birth.In this work, we formalize PfB and design Verified Remote Sensing Authorization (VERSA) – a provably secure and formally verified architecture guaranteeing that only correct execution of expected and explicitly authorized software can access and manipulate sensing interfaces, specifically, General Purpose Input/Output (GPIO), which is the usual boundary between analog and digital worlds on IoT devices. This guarantee is obtained with minimal hardware support and holds even if all device software is compromised. VERSA ensures that malware can neither gain access to sensed data on the GPIO-mapped memory nor obtain any trace thereof. VERSA formally verified and its open-sourced implementation targets resource-constrained IoT edge devices, commonly used for sensing. Experimental results show that PfB is both achievable and affordable for such devices.