A Logic for Information Flow Analysis of Distributed Programs
2013 (English)In: Secure IT Systems: 18th Nordic Conference, NordSec 2013 Ilulissat, Greenland, October 2013 Proceedings, Springer Berlin/Heidelberg, 2013, 84-99 p.Conference paper (Refereed)
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
Springer Berlin/Heidelberg, 2013. 84-99 p.
, Lecture Notes in Computer Science, ISSN 0302-9743 ; 8208
possibilistic information flow, logic of knowledge, languagebased security, verification
IdentifiersURN: urn:nbn:se:kth:diva-136195DOI: 10.1007/978-3-642-41488-6ISI: 000340414300006ScopusID: 2-s2.0-84890869056ISBN: 978-3-642-41488-6OAI: oai:DiVA.org:kth-136195DiVA: diva2:675561
18th Nordic Conference on Secure IT Systems, NordSec 2013; Ilulissat; Greenland; 18 October 2013 through 21 October 2013
QC 201312192013-12-042013-12-042014-09-11Bibliographically approved