Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • harvard1
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf
Logics for Information Flow Security:From Specification to Verification
KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
2014 (English)Doctoral thesis, comprehensive summary (Other academic)
Abstract [en]

Software is becoming  increasingly  ubiquitous and today we find software running everywhere. There is software driving our favorite  game  application or  inside the web portal we use to read the morning  news, and   when we book a vacation.  Being so commonplace, software has become an easy target to compromise  maliciously or at best to get it wrong. In fact, recent trends and highly-publicized attacks suggest that vulnerable software  is at  the root of many security attacks.     

Information flow security is the research field that studies  methods and techniques to provide strong security guarantees against  software security attacks and vulnerabilities.  The goal of an  information flow analysis is to rigorously check how  sensitive information is used by the software application and ensure that this information does not escape the boundaries of the application, unless it is properly granted permission to do so by the security policy at hand.  This process can   be challenging asit first requires to determine what the applications security policy is and then to provide a mechanism  to enforce that policy against the  software application.  In this thesis  we address the problem of (information flow) policy specification and policy enforcement by leveraging formal methods, in particular logics and language-based analysis and verification techniques.

The thesis contributes to the state of the art of information flow security in several directions, both theoretical and practical. On the policy specification side, we provide a  framework to reason about  information flow security conditions using the notion of knowledge. This is accompanied  by logics that  can be used  to express the security policies precisely in a syntactical manner. Also, we study the interplay between confidentiality and integrity  to enforce security in  presence of active attacks.  On the verification side, we provide several symbolic algorithms to effectively check whether an application adheres to the associated security policy. To achieve this,  we propose techniques  based on symbolic execution and first-order reasoning (SMT solving) to first extract a model of the target application and then verify it against the policy.  On the practical side, we provide  tool support by automating our techniques and  thereby making it possible  to verify programs written in Java or ARM machine code.  Besides the expected limitations, our case studies show that the tools can be used to  verify the security of several realistic scenarios.

More specifically, the thesis consists of two parts and six chapters. We start with an introduction giving an overview of the research problems and the results of the thesis. Then we move to the specification part which  relies on knowledge-based reasoning and epistemic logics to specify state-based and trace-based information flow conditions and on the weakest precondition calculus to certify security in  presence of active attacks.  The second part of the thesis addresses the problem of verification  of the security policies introduced in the first part.  We use symbolic execution  and  SMT solving techniques to enable   model checking of the security properties.  In particular, we implement a tool that verifies noninterference  and declassification policies for Java programs. Finally, we conclude with relational verification of low level code, which is also supported by a tool.

Place, publisher, year, edition, pages
Stockholm: KTH Royal Institute of Technology, 2014. , viii, 127 p.
Series
TRITA-CSC-A, ISSN 1653-5723 ; 2014:13
National Category
Computer Systems
Research subject
Computer Science
Identifiers
URN: urn:nbn:se:kth:diva-150423ISBN: 978-91-7595-259-8 (print)OAI: oai:DiVA.org:kth-150423DiVA: diva2:743274
Public defence
2014-10-03, Kollegiesalen, Brinellvägen 8, KTH, Stockholm, 14:00 (English)
Opponent
Supervisors
Note

QC 20140908

Available from: 2014-09-08 Created: 2014-09-03 Last updated: 2014-09-08Bibliographically approved
List of papers
1. Epistemic Temporal Logic for Information Flow Security
Open this publication in new window or tab >>Epistemic Temporal Logic for Information Flow Security
2011 (English)In: In proc. of th 4e ACM SIGPLAN workshop on Programming Languages and Analysis for Security, 2011Conference paper, Published paper (Refereed)
Abstract [en]

Temporal epistemic logic is a well-established framework for expressing agents knowledge and how it evolves over time. Within language-based security these are central issues, for instance in the context of declassification. We propose to bring these two areas together. The paper presents a computational model and an epistemic temporal logic used to reason about knowledge acquired by observing program outputs. This approach is shown to elegantly capture standard notions of noninterference and declassification in the literature as well as information flow properties where sensitive and public data intermingle in delicate ways.

Keyword
Security, Information Flow, Epistemic Logic
National Category
Computer and Information Science
Identifiers
urn:nbn:se:kth:diva-50299 (URN)10.1145/2166956.2166962 (DOI)2-s2.0-84860284337 (Scopus ID)978-145030830-4 (ISBN)
Conference
ACM SIGPLAN Sixth Workshop on Programming Languages and Analysis for Security (PLAS 2011). San Jose, USA. June 05 2011
Funder
ICT - The Next Generation
Note

QC 20111208

Available from: 2011-12-05 Created: 2011-12-05 Last updated: 2014-09-08Bibliographically approved
2. A Logic for Information Flow Analysis of Distributed Programs
Open this publication in new window or tab >>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, Published paper (Refereed)
Abstract [en]

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
Series
Lecture Notes in Computer Science, ISSN 0302-9743 ; 8208
Keyword
possibilistic information flow, logic of knowledge, languagebased security, verification
National Category
Computer Science
Identifiers
urn:nbn:se:kth:diva-136195 (URN)10.1007/978-3-642-41488-6 (DOI)000340414300006 ()2-s2.0-84890869056 (Scopus ID)978-3-642-41488-6 (ISBN)
Conference
18th Nordic Conference on Secure IT Systems, NordSec 2013; Ilulissat; Greenland; 18 October 2013 through 21 October 2013
Note

QC 20131219

Available from: 2013-12-04 Created: 2013-12-04 Last updated: 2014-09-11Bibliographically approved
3. A Weakest Precondition Approach to Robustness
Open this publication in new window or tab >>A Weakest Precondition Approach to Robustness
2010 (English)In: Lecture Notes in Computer Science, ISSN 0302-9743, E-ISSN 1611-3349, Vol. 6340, no PART 1, 261-297 p.Article in journal (Refereed) Published
Abstract [en]

With the increasing complexity of information management computer systems, security becomes a real concern. E-government, web-based financial transactions or military and health care information systems are only a few examples where large amount of information can reside on different hosts distributed worldwide. It is clear that any disclosure or corruption of confidential information in these contexts can result fatal. Information flow controls constitute an appealing and promising technology to protect both data confidentiality and data integrity. The certification of the security degree of a program that runs in untrusted environments still remains an open problem in the area of language-based security. Robustness asserts that an active attacker, who can modify program code in some fixed points (holes), is unable to disclose more private information than a passive attacker, who merely observes unclassified data. In this paper, we extend a method recently proposed for checking declassified non-interference in presence of passive attackers only, in order to check robustness by means of weakest precondition semantics. In particular, this semantics simulates the kind of analysis that can be performed by an attacker, i.e., from public output towards private input. The choice of semantics allows us to distinguish between different attacks models and to characterize the security of applications in different scenarios. Our results are sound to address confidentiality and integrity of software running in untrusted environments where different actors can distrust one another. For instance, a web server can be attacked by a third party in order to steal a session cookie or hijack clients to a fake web page.

Keyword
abstract interpretation, active attackers, declassification, non-interference, program semantics, robustness, security
National Category
Computer Science
Identifiers
urn:nbn:se:kth:diva-81050 (URN)10.1007/978-3-642-17499-5_11 (DOI)2-s2.0-78650666141 (Scopus ID)
Note
QC 20120216Available from: 2012-02-10 Created: 2012-02-10 Last updated: 2017-12-07Bibliographically approved
4. ENCOVER: Symbolic Exploration for Information Flow Security
Open this publication in new window or tab >>ENCOVER: Symbolic Exploration for Information Flow Security
2012 (English)In: 2012 IEEE 25th Computer Security Foundations Symposium (CSF), IEEE , 2012, 30-44 p.Conference paper, Published paper (Refereed)
Abstract [en]

We address the problem of program verification for information flow policies by means of symbolic execution and model checking. Noninterference-like security policies are formalized using epistemic logic. We show how the policies can be accurately verified using a combination of concolic testing and SMT solving. As we demonstrate, many scenarios considered tricky in the literature can be solved precisely using the proposed approach. This is confirmed by experiments performed with ENCOVER, a tool based on Java PathFinder and Z3, which we have developed for epistemic noninterference concolic verification.

Place, publisher, year, edition, pages
IEEE, 2012
Series
Proceedings-Computer Security Foundations Workshop, ISSN 1063-6900
Keyword
information flow security, noninterference, model checking, epistemic logic, SMT solver, declassification
National Category
Computer and Information Science
Identifiers
urn:nbn:se:kth:diva-104390 (URN)10.1109/CSF.2012.24 (DOI)000309007800003 ()2-s2.0-84866898679 (Scopus ID)978-0-7695-4718-3 (ISBN)
Conference
25th IEEE Computer Security Foundations Symposium (CSF), JUN 25-27, 2012, Cambridge, MA
Funder
ICT - The Next Generation
Note

QC 20121101

Available from: 2012-11-01 Created: 2012-11-01 Last updated: 2014-09-08Bibliographically approved
5. Automating Information Flow Analysis of Low Level Code
Open this publication in new window or tab >>Automating Information Flow Analysis of Low Level Code
2014 (English)In: Proceedings of CCS’14, November 3–7, 2014, Scottsdale, Arizona, USA, Association for Computing Machinery (ACM), 2014Conference paper, Published paper (Refereed)
Abstract [en]

Low level code is challenging: It lacks structure, it uses jumps and symbolic addresses, the control ow is often highly optimized, and registers and memory locations may be reused in ways that make typing extremely challenging. Information ow properties create additional complications: They are hyperproperties relating multiple executions, and the possibility of interrupts and concurrency, and use of devices and features like memory-mapped I/O requires a departure from the usual initial-state nal-state account of noninterference. In this work we propose a novel approach to relational verication for machine code. Verication goals are expressed as equivalence of traces decorated with observation points. Relational verication conditions are propagated between observation points using symbolic execution, and discharged using rst-order reasoning. We have implemented an automated tool that integrates with SMT solvers to automate the verication task. The tool transforms ARMv7 binaries into an intermediate, architecture-independent format using the BAP toolset by means of a veried translator. We demonstrate the capabilities of the tool on a separation kernel system call handler, which mixes hand-written assembly with gcc-optimized output, a UART device driver and a crypto service modular exponentiation routine.

Place, publisher, year, edition, pages
Association for Computing Machinery (ACM), 2014
Keyword
Information Flow Security, Formal Verification, Symbolic Execution;, Machine Code
National Category
Computer Systems
Identifiers
urn:nbn:se:kth:diva-150489 (URN)10.1145/2660267.2660322 (DOI)2-s2.0-84910645826 (Scopus ID)978-1-4503-2957-6 (ISBN)
Conference
CCS’14, November 3–7, 2014, Scottsdale, Arizona, USA
Note

QC 20140905

Available from: 2014-09-04 Created: 2014-09-04 Last updated: 2014-09-08Bibliographically approved

Open Access in DiVA

php-thesis-Musard-Balliu(1540 kB)670 downloads
File information
File name FULLTEXT04.pdfFile size 1540 kBChecksum SHA-512
b4b6070d9d008770240da4225814ddfb4809bade9ce1d9cbf84cb8372d264074c169ed7f5c4db457e330b6950c651d206933ed39b214dd34e05dcdc93de58690
Type fulltextMimetype application/pdf

Search in DiVA

By author/editor
Balliu, Musard
By organisation
Theoretical Computer Science, TCS
Computer Systems

Search outside of DiVA

GoogleGoogle Scholar
Total: 676 downloads
The number of downloads is the sum of all downloads of full texts. It may include eg previous versions that are now no longer available

isbn
urn-nbn

Altmetric score

isbn
urn-nbn
Total: 2322 hits
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • harvard1
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf