### Skapa referens, olika format (klipp och klistra)

**Harvard**

Vassena, M. och Russo, A. (2016) *On formalizing information-flow control libraries*. : Association for Computing Machinery, Inc

** BibTeX **

@conference{

Vassena2016,

author={Vassena, Marco and Russo, Alejandro},

title={On formalizing information-flow control libraries},

booktitle={11th ACM SIGSAC Workshop on Programming Languages and Analysis for Security, PLAS 2016, Vienna, Austria, 24 October 2016},

isbn={9781450345743 },

pages={15-28},

abstract={Many state-of-the-art IFC libraries support a variety of advanced features like mutuable data structures, exceptions, and concurrency, whose subtle interaction makes verification of security guarantees challenging. In this paper, we present a full-fledged, mechanically-verifiedmodel of MAC-a statically enforced IFC library. We describe three main insights gained during the formalization process. As previous libraries (e.g., LIO and HLIO), we utilize term erasure as the proof technique to show non-interference. This technique essentially states that the same public output should be produced if secrets are erased before or after program execution. Our first insight identifies challenges when the sensitivity of terms may depend on the context where they are used, thus affecting how they will be erased. This situation is not uncommon in MAC as well as other IFC libraries-in fact, we spot problems in the proofs of previous work. To deal with such complicated situations, we propose a novel erasure technique that performs erasure by additional evaluation rules, triggered by special-purpose constructs. Furthermore, we simplify reasoning about exception-aware primitives by removing sensitive exceptions from programs where secrets have been erased. We show progress insensitive noninterference for our sequential calculus and pinpoint sufficient requirements on the scheduler to prove progress-sensitive non-interference for our concurrent calculus. We prove that MAC is secure under a round-robin scheduler by simply instantiating our main scheduler-parametric theorem. },

publisher={Association for Computing Machinery, Inc},

year={2016},

keywords={Agda, Haskell, Non-interference, Calculations, Libraries, Object oriented programming, Routers, Scheduling, Concurrent calculi, Information flow control, Non interference, Round robin schedulers, Sequential calculus, Subtle interaction, Concurrency control },

}

** RefWorks **

RT Conference Proceedings

SR Electronic

ID 247397

A1 Vassena, Marco

A1 Russo, Alejandro

T1 On formalizing information-flow control libraries

YR 2016

T2 11th ACM SIGSAC Workshop on Programming Languages and Analysis for Security, PLAS 2016, Vienna, Austria, 24 October 2016

SN 9781450345743

SP 15

OP 28

AB Many state-of-the-art IFC libraries support a variety of advanced features like mutuable data structures, exceptions, and concurrency, whose subtle interaction makes verification of security guarantees challenging. In this paper, we present a full-fledged, mechanically-verifiedmodel of MAC-a statically enforced IFC library. We describe three main insights gained during the formalization process. As previous libraries (e.g., LIO and HLIO), we utilize term erasure as the proof technique to show non-interference. This technique essentially states that the same public output should be produced if secrets are erased before or after program execution. Our first insight identifies challenges when the sensitivity of terms may depend on the context where they are used, thus affecting how they will be erased. This situation is not uncommon in MAC as well as other IFC libraries-in fact, we spot problems in the proofs of previous work. To deal with such complicated situations, we propose a novel erasure technique that performs erasure by additional evaluation rules, triggered by special-purpose constructs. Furthermore, we simplify reasoning about exception-aware primitives by removing sensitive exceptions from programs where secrets have been erased. We show progress insensitive noninterference for our sequential calculus and pinpoint sufficient requirements on the scheduler to prove progress-sensitive non-interference for our concurrent calculus. We prove that MAC is secure under a round-robin scheduler by simply instantiating our main scheduler-parametric theorem.

PB Association for Computing Machinery, Inc

LA eng

DO 10.1145/2993600.2993608

LK http://dx.doi.org/10.1145/2993600.2993608

OL 30