-
Meta-level issues in Offloading: Sco**, Composition, Development, and their Automation
Authors:
André DeHon,
Hans Giesen,
Nik Sultana,
Yuanlong Xiao
Abstract:
This paper argues for an accelerator development toolchain that takes into account the whole system containing the accelerator. With whole-system visibility, the toolchain can better assist accelerator sco** and composition in the context of the expected workloads and intended performance objectives. Despite being focused on the 'meta-level' of accelerators, this would build on existing and ongo…
▽ More
This paper argues for an accelerator development toolchain that takes into account the whole system containing the accelerator. With whole-system visibility, the toolchain can better assist accelerator sco** and composition in the context of the expected workloads and intended performance objectives. Despite being focused on the 'meta-level' of accelerators, this would build on existing and ongoing DSLs and toolchains for accelerator design. Basing this on our experience in programmable networking and reconfigurable-hardware programming, we propose an integrative approach that relies on three activities: (i) generalizing the focus of acceleration to offloading to accommodate a broader variety of non-functional needs -- such as security and power use -- while using similar implementation approaches, (ii) discovering what to offload, and to what hardware, through semi-automated analysis of a whole system that might compose different offload choices that changeover time, (iii) connecting with research and state-of-the-art approaches for using domain-specific languages (DSLs) and high-level synthesis (HLS) systems for custom offload development. We outline how this integration can drive new development tooling that accepts models of programs and resources to assist system designers through design-space exploration for the accelerated system.
△ Less
Submitted 5 April, 2021;
originally announced April 2021.
-
Mir: Automated Quantifiable Privilege Reduction Against Dynamic Library Compromise in JavaScript
Authors:
Nikos Vasilakis,
Cristian-Alexandru Staicu,
Grigoris Ntousakis,
Konstantinos Kallas,
Ben Karel,
André DeHon,
Michael Pradel
Abstract:
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…
▽ More
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.
△ Less
Submitted 1 January, 2021; v1 submitted 31 October, 2020;
originally announced November 2020.
-
A Verified Information-Flow Architecture
Authors:
Arthur Azevedo de Amorim,
Nathan Collins,
André DeHon,
Delphine Demange,
Catalin Hritcu,
David Pichardie,
Benjamin C. Pierce,
Randy Pollack,
Andrew Tolmach
Abstract:
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…
▽ More
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.
△ Less
Submitted 6 March, 2016; v1 submitted 22 September, 2015;
originally announced September 2015.
