Source author record

André DeHon

André DeHon appears in the imported research catalog. Authorship, coauthor and topic links are available while profile ownership is still unclaimed.

ResearcherUnclaimed source record

Catalog footprint

What is connected

2works
2topics
4close collaborators

Actions

Connect this record

Log in to claim

Research graph

See the researcher in context

Open full explorer

Inspect adjacent papers, topics, institutions and collaborators without losing the researcher page.

Building this map preview

BZPEER is loading the nearby papers, people, topics and institutions for this page.

Published work

2 published item(s)

preprint2021arXiv

Mir: Automated Quantifiable Privilege Reduction Against Dynamic Library Compromise in JavaScript

Third-party libraries ease the development of large-scale software systems. However, they often execute with significantly more privilege than needed to complete their task. This additional privilege is often exploited at runtime via dynamic compromise, even when these libraries are not actively malicious. Mir addresses this problem by introducing a fine-grained read-write-execute (RWX) permission model at the boundaries of libraries. Every field of an imported library is governed by a set of permissions, which developers can express when importing libraries. To enforce these permissions during program execution, Mir transforms libraries and their context to add runtime checks. As permissions can overwhelm developers, Mir's permission inference generates default permissions by analyzing how libraries are used by their consumers. Applied to 50 popular libraries, Mir's prototype for JavaScript demonstrates that the RWX permission model combines simplicity with power: it is simple enough to automatically infer 99.33% of required permissions, it is expressive enough to defend against 16 real threats, it is efficient enough to be usable in practice (1.93% overhead), and it enables a novel quantification of privilege reduction.

preprint2016arXiv

A Verified Information-Flow Architecture

SAFE is a clean-slate design for a highly secure computer system, with pervasive mechanisms for tracking and limiting information flows. At the lowest level, the SAFE hardware supports fine-grained programmable tags, with efficient and flexible propagation and combination of tags as instructions are executed. The operating system virtualizes these generic facilities to present an information-flow abstract machine that allows user programs to label sensitive data with rich confidentiality policies. We present a formal, machine-checked model of the key hardware and software mechanisms used to dynamically control information flow in SAFE and an end-to-end proof of noninterference for this model. We use a refinement proof methodology to propagate the noninterference property of the abstract machine down to the concrete machine level. We use an intermediate layer in the refinement chain that factors out the details of the information-flow control policy and devise a code generator for compiling such information-flow policies into low-level monitor code. Finally, we verify the correctness of this generator using a dedicated Hoare logic that abstracts from low-level machine instructions into a reusable set of verified structured code generators.