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
ENCOVER: Symbolic Exploration for Information Flow Security
KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.ORCID iD: 0000-0001-5432-6442
KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
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. 30-44 p.
Series
Proceedings-Computer Security Foundations Workshop, ISSN 1063-6900
Keyword [en]
information flow security, noninterference, model checking, epistemic logic, SMT solver, declassification
National Category
Computer and Information Science
Identifiers
URN: urn:nbn:se:kth:diva-104390DOI: 10.1109/CSF.2012.24ISI: 000309007800003Scopus ID: 2-s2.0-84866898679ISBN: 978-0-7695-4718-3 (print)OAI: oai:DiVA.org:kth-104390DiVA: diva2:564473
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
In thesis
1. Logics for Information Flow Security:From Specification to Verification
Open this publication in new window or tab >>Logics for Information Flow Security:From Specification to Verification
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:nbn:se:kth:diva-150423 (URN)978-91-7595-259-8 (ISBN)
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

Open Access in DiVA

No full text

Other links

Publisher's full textScopus

Authority records BETA

Dam, Mads

Search in DiVA

By author/editor
Balliu, MusardDam, MadsLe Guernic, Gurvan
By organisation
Theoretical Computer Science, TCS
Computer and Information Science

Search outside of DiVA

GoogleGoogle Scholar

doi
isbn
urn-nbn

Altmetric score

doi
isbn
urn-nbn
Total: 130 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