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

A Library for Secure Multi-threaded Information Flow in Haskell

Tsa-chung Tsai (Institutionen för data- och informationsteknik, Datavetenskap (Chalmers)) ; Alejandro Russo (Institutionen för data- och informationsteknik, Datavetenskap (Chalmers)) ; John Hughes (Institutionen för data- och informationsteknik, Datavetenskap (Chalmers))
Proceedings of the 20th IEEE Computer Security Foundations Symposium. IEEE Computer Society Press. (2007)
[Konferensbidrag, refereegranskat]

Li and Zdancewic have recently proposed an approach to provide information-flow security via a library rather than producing a new language from the scratch. They have shown how to implement such a library in Haskell by using arrow combinators. However, their approach only works with computations that have no side-effects. In fact, they leave as an open question how their library, and the mechanisms in it, need to be modified to consider these kind of effects. Another absent feature in the library is support for multithreaded programs. Information-flow in multithreaded programs still remains as a challenge, and no support for that has been implemented yet. It is not surprising, then, that the two main stream compilers that provide information-flow security, Jif and FlowCaml, lack support for multithreading. Following ideas taken from literature, this paper presents an extension to Li and Zdancewic’s library that provides information-flow security in presence of reference manipulation and multithreaded programs. Moreover, an online shopping case study has been implemented to evaluate the proposed techniques. The case study reveals that exploiting concurrency to leak secrets is feasible and dangerous in practice and how our extension helps avoiding that. To the best of our knowledge, this is the first implemented tool to guarantee information-flow security in concurrent programs and the first implementation of a case study that involves concurrency and information-flow policies.



Denna post skapades 2007-06-14.
CPL Pubid: 42756

 

Läs direkt!


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


Institutioner (Chalmers)

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

Ämnesområden

Datalogi

Chalmers infrastruktur

Relaterade publikationer

Denna publikation ingår i:


Language Support for Controlling Timing-Based Covert Channels