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

HLIO: Mixing Static and Dynamic Typing for Information-Flow Control in Haskell

Pablo Buiras (Institutionen för data- och informationsteknik, Programvaruteknik (Chalmers)) ; Dimitrios Vytiniotis ; Alejandro Russo (Institutionen för data- och informationsteknik, Programvaruteknik (Chalmers))
Proceedings of the 20th ACM SIGPLAN International Conference on Functional Programming (0362-1340). Vol. 50 (2015), 9, p. 289-301 .
[Konferensbidrag, refereegranskat]

Information-Flow Control (IFC) is a well-established approach for allowing untrusted code to manipulate sensitive data without disclosing it. IFC is typically enforced via type systems and static analyses or via dynamic execution monitors. The LIO Haskell library, originating in operating systems research, implements a purely dynamic monitor of the sensitivity level of a computation, particularly suitable when data sensitivity levels are only known at runtime. In this paper, we show how to give programmers the flexibility of deferring IFC checks to runtime (as in LIO), while also providing static guarantees---and the absence of runtime checks---for parts of their programs that can be statically verified (unlike LIO). We present the design and implementation of our approach, HLIO (Hybrid LIO), as an embedding in Haskell that uses a novel technique for deferring IFC checks based on singleton types and constraint polymorphism. We formalize HLIO, prove non-interference, and show how interesting IFC examples can be programmed. Although our motivation is IFC, our technique for deferring constraints goes well beyond and offers a methodology for programmer-controlled hybrid type checking in Haskell.

Nyckelord: Information-flow control, hybrid typing, gradual typing, dynamic typing, data kinds, constraint kinds, singleton types



Den här publikationen ingår i följande styrkeområden:

Läs mer om Chalmers styrkeområden  

Denna post skapades 2015-09-29. Senast ändrad 2016-11-02.
CPL Pubid: 223373

 

Läs direkt!


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