CPL - Chalmers Publication Library
| Utbildning | Forskning | Styrkeområden | Om Chalmers | In English In English Ej inloggad.

On formalizing information-flow control libraries

Marco Vassena (Institutionen för data- och informationsteknik, Programvaruteknik (Chalmers)) ; Alejandro Russo (Institutionen för data- och informationsteknik, Programvaruteknik (Chalmers))
11th ACM SIGSAC Workshop on Programming Languages and Analysis for Security, PLAS 2016, Vienna, Austria, 24 October 2016 p. 15-28. (2016)
[Konferensbidrag, refereegranskat]

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.

Nyckelord: 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

Denna post skapades 2017-01-19. Senast ändrad 2017-02-03.
CPL Pubid: 247397


Läs direkt!

Länk till annan sajt (kan kräva inloggning)

Institutioner (Chalmers)

Institutionen för data- och informationsteknik, Programvaruteknik (Chalmers)



Chalmers infrastruktur

Relaterade publikationer

Denna publikation ingår i:

MAC, A Verified Information-Flow Control Library