A Logic for Information Flow Analysis of Distributed Programs: (Extended Abstract)
2013 (English)Report (Other academic)
Securing communication in large scale distributed systems is an open problem. When multiple principals exchange sensitive information over a network, security and privacy issues arise immediately. For instance, in an online auction system we may want to ensure that no bidder knows the bids of any other bidder before the auction is closed. Such systems are typically interactive/reactive and communication is mostly asynchronous, lossy or unordered. Language-based security provides language mechanisms for enforcing end-to-end security. However, with few exceptions, previous research has mainly focused on relational or synchronous models, which are generally not suitable for distributed systems.
This paper proposes a general knowledge-based account of possibilistic security from a language perspective and shows how existing trace-based conditions fit in. A syntactic characterization of these conditions, given by an epistemic temporal logic, shows that existing model checking tools can be used to enforce security.
Place, publisher, year, edition, pages
KTH Royal Institute of Technology, 2013. , 19 p.
possibilistic information flow, logic of knowledge, language-based security, verification
Electrical Engineering, Electronic Engineering, Information Engineering
IdentifiersURN: urn:nbn:se:kth:diva-124418OAI: oai:DiVA.org:kth-124418DiVA: diva2:635362
QC 201307102013-07-032013-07-032013-07-10Bibliographically approved