log in  |  register  |  feedback?  |  help  |  web accessibility
Logo
End-to-End Information-Flow Security for Interactive Systems
Wednesday, September 24, 2014, 11:00 am-12:00 pm Calendar
  • You are subscribed to this talk through .
  • You are watching this talk through .
  • You are subscribed to this talk. (unsubscribe, watch)
  • You are watching this talk. (unwatch, subscribe)
  • You are not subscribed to this talk. (watch, subscribe)
Abstract
We provide means to achieve end-to-end information-flow security in interactive systems. In a general computation model for asynchronous message-passing components, we consider two popular confidentiality properties: progress-sensitive noninterference (PSNI), and progress-insensitive noninterference (PINI), the latter of which is enforced by practical tools like JSFlow, Paragon, Jif, FlowCaml, SPARK, and sequential LIO. After identifying shortcomings in previous formalizations of PSNI and PINI, we devise a new, preservation-based, formalization which guarantees secure systems interact securely. We prove this compositionality guarantee for a dataflow-style core of combinators, and derive a rich language of security-preserving combinators from it. While both PSNI and PINI are preserved under arbitrary wirings, PINI fundamentally relies on the lack of scheduling fairness to guarantee security of interactions. This makes PINI unfit for autonomous interactive systems security. To facilitate building secure systems in parts, we advance secure multi-execution (SME): a combinator which repairs insecurities. SME thus makes any interactive system, secure or not, readily pluggable into a secure composite system. We prove soundness for all fair schedulers, and redesign SME to enforce PSNI, obtaining a more semantics-preserving combinator. We furthermore give a model for information release in SME. Finally, for scenarios where semantics must be preserved, we demonstrate how PSNI and PINI can be enforced statically by a type-based enforcement. Save for our static enforcements, all our results are language-independent.
This talk is organized by Kristopher Micinski