@inproceedings{DoerreKlebanov15,
author = {Felix D{\"o}rre and Vladimir Klebanov},
title = {Pseudo-Random Number Generator Verification: A Case Study},
booktitle = {Proceedings, Verified Software: Theories, Tools, and Experiments (VSTTE)},
editor = {Arie Gurfinkel and Sanjit A. Seshia},
year = 2015,
publisher = {Springer},
series = {Lecture Notes in Computer Science}
}
@inproceedings{KuestersTruderungBeckertEtAl15,
author = {Ralf K{\"u}sters and Tomasz Truderung and Bernhard Beckert
and Daniel Bruns and Michael Kirsten and Martin Mohr},
title = {A Hybrid Approach for Proving Noninterference of {Java}
Programs},
booktitle = {28th IEEE Computer Security Foundations Symposium},
editor = {C{\'e}dric Fournet and Michael Hicks},
year = 2015,
abstract = {Several tools and approaches for proving noninterference
properties for Java and other languages exist. Some of them
have a high degree of automation or are even fully
automatic, but overapproximate the actual information flow,
and hence, may produce false positives. Other tools, such
as those based on theorem proving, are precise, but may
need interaction, and hence, analysis is time-consuming.
In this paper, we propose a hybrid approach that aims at
obtaining the best of both approaches: We want to use fully
automatic analysis as much as possible and only at places
in a program where, due to overapproximation, the automatic
approaches fail, we resort to more precise, but interactive
analysis, where the latter involves only the verification
of specific functional properties in certain parts of the
program, rather than checking more intricate
noninterference properties for the whole program.
To illustrate the hybrid approach, in a case study we use
the hybrid approach---along with the fully automatic tool
Joana for checking noninterference properties for Java
programs and the theorem prover \KeY for the verification
of Java programs---and the CVJ framework proposed by
K\"usters, Truderung, and Graf to establish cryptographic
privacy properties for a non-trivial Java program, namely
an e-voting system. The CVJ framework allows one to
establish cryptographic indistinguishability properties for
Java programs by checking (standard) noninterference
properties for such programs.}
}
@inproceedings{BrunsDoGreinerEtAl15,
author = {Daniel Bruns and Huy Quoc Do and Simon Greiner and Mihai
Herda and Martin Mohr and Enrico Scapin and Tomasz
Truderung and Bernhard Beckert and Ralf K{\"u}sters and
Heiko Mantel and Richard Gay},
title = {Poster: {Security} in E-Voting},
booktitle = {36th IEEE Symposium on Security and Privacy, Poster
Session},
editor = {Sophie Engle},
year = 2015,
month = may # {~18}
}
@inproceedings{Bruns15a,
author = {Daniel Bruns},
title = {A Theorem Proving Approach to Secure Information Flow in
Concurrent Programs (extended abstract)},
booktitle = {Workshop on Foundations of Computer Security (FCS~2015)},
editor = {Deepak Garg and Boris K{\"o}pf},
language = {english},
year = 2015,
month = jul,
url = {http://software.imdea.org/~bkoepf/FCS15/paper3.pdf}
}
@inproceedings{BeckertBrunsKlebanovEtAl14,
author = {Bernhard Beckert and Daniel Bruns and Vladimir Klebanov
and Christoph Scheben and Peter H. Schmitt and Mattias
Ulbrich},
title = {Information Flow in Object-Oriented Software},
booktitle = {Logic-Based Program Synthesis and Transformation, LOPSTR
2013},
editor = {Gopal Gupta and Ricardo Pe{\~n}a},
year = 2014,
publisher = {Springer},
series = {Lecture Notes in Computer Science},
number = 8901,
pages = {19--37},
doi = {10.1007/978-3-319-14125-1_2},
isbn = {978-3-319-14125-1},
abstract = {This paper contributes to the investigation of
object-sensitive information-flow properties for sequential
Java, i.e., properties that take into account information
leakage through objects, as opposed to primitive values. We
present two improvements to a popular object-sensitive
non-interference property. Both reduce the burden on
analysis and monitoring tools. The second contribution is a
formalization of this property in a program logic -- JavaDL
in our case -- which allows using an existing tool without
requiring program modification. The third contribution is a
novel fine-grained specification methodology. In our
approach, arbitrary JavaDL terms (read side-effect-free
Java expressions) may be assigned a security level -- in
contrast to security labels being attached to fields and
variables only. }
}
@inproceedings{AhrendtBeckertBrunsEtAl14,
author = {Ahrendt, Wolfgang and Beckert, Bernhard and Bruns, Daniel
and Bubel, Richard and Gladisch, Christoph and Grebing,
Sarah and H{\"a}hnle, Reiner and Hentschel, Martin and
Herda, Mihai and Klebanov, Vladimir and Mostowski, Wojciech
and Scheben, Christoph and Schmitt, Peter H. and Ulbrich,
Mattias},
title = {The {KeY} Platform for Verification and Analysis of
{Java} Programs},
year = 2014,
booktitle = {Verified Software: Theories, Tools, and Experiments (VSTTE
2014)},
language = {english},
editor = {Giannakopoulou, Dimitra and Kroening, Daniel},
pages = {1--17},
publisher = {Springer-Verlag},
number = 8471,
series = {Lecture Notes in Computer Science},
isbn = {978-3-642-54107-0},
doi = {10.1007/978-3-319-12154-3_4},
url = {http://link.springer.com/chapter/10.1007/978-3-319-12154-3_4},
abstract = {The \KeY\ system offers a platform of software analysis
tools for sequential Java. Foremost, this includes full
functional verification against contracts written in the
Java Modeling Language. But the approach is general enough
to provide a basis for other methods and purposes: (i)
complementary validation techniques to formal verification
such as testing and debugging, (ii) methods that reduce the
complexity of verification such as modularization and
abstract interpretation, (iii) analyses of non-functional
properties such as information flow security, and (iv)
sound program transformation and code generation. We show
that deductive technology that has been developed for full
functional verification can be used as a basis and
framework for other purposes than pure functional
verification. We use the current release of the \KeY\
system as an example to explain and prove this claim.}
}
@inproceedings{beckert.bruns.ea12,
author = {Bernhard Beckert and Daniel Bruns and Sarah Grebing},
title = {Mind the Gap: Formal Verification and the {Common}
{Criteria}},
year = 2012,
booktitle = {6th~International Verification Workshop, VERIFY-2010},
address = {Edinburgh, United Kingdom},
editor = {Markus Aderhold and Serge Autexier and Heiko Mantel},
abstract = {It is a common belief that the rise of standardized
software certification schemes like the Common Criteria
(CC) would give a boost to formal verification, and that
software certification may be a killer application for
program verification. However, while formal models are
indeed used throughout high-assurance certification,
verification of the actual implementation is not required
by the CC and largely neglected in certification practice
-- despite the great advances in program verification over
the last decade. In this paper we discuss the gap between
program verification and CC software certification, and we
point out possible uses of code-level program verification
in the CC certification process.},
series = {EPiC Series},
volume = {3},
pages = {4-12},
publisher = {EasyChair},
issn = {2040-557X},
note = {Discussion paper},
url = {http://easychair.org/publications/?page=1489979161}
}
@incollection{scheben.schmitt12,
author = {Scheben, Christoph and Schmitt, Peter H.},
title = {Verification of Information Flow Properties of {J}ava
Programs without Approximations},
booktitle = {Formal Verification of Object-Oriented Software},
series = {LNCS},
volume = {7421},
publisher = {Springer},
pages = {232--249},
year = {2012}
}
@inproceedings{Klebanov12a,
author = {Vladimir Klebanov},
title = {Precise Quantitative Information Flow Analysis Using Symbolic Model Counting},
editor = {Fabio Martinelli and Flemming Nielson},
booktitle = {Proceedings, International Workshop on Quantitative Aspects in Security Assurance (QASA)},
year = {2012},
url = {http://formal.iti.kit.edu/~klebanov/pubs/qasa2012.pdf}
}
@inproceedings{beckert.bruns13,
author = {Bernhard Beckert and Daniel Bruns},
title = {Dynamic Logic with Trace Semantics},
booktitle = {24th International Conference on Automated Deduction
(CADE-24)},
editor = {Maria Paola Bonacina},
year = 2013,
publisher = {Springer-Verlag},
series = {Lecture Notes in Computer Science},
volume = 7898,
pages = {315--329},
isbn = {978-3-642-38573-5},
doi = {10.1007/978-3-642-38574-2_22},
url = {http://link.springer.com/chapter/10.1007/978-3-642-38574-2_22},
abstract = {Dynamic logic is an established instrument for program
verification and for reasoning about the semantics of
programs and programming languages. In this paper, we
define an extension of dynamic logic, called Dynamic Trace
Logic~(DTL), which combines the expressiveness of program
logics such as dynamic logic with that of temporal logic.
And we present a sound and relatively complete sequent
calculus for proving validity of DTL formulae. Due to its
expressiveness, DTL can serve as a basis for proving
functional and information-flow properties in concurrent
programs, among other applications.}
}
@inproceedings{kusters.truderung.ea13,
author = {Ralf K{\"u}sters and Tomasz Truderung and Bernhard Beckert
and Daniel Bruns and J{\"u}rgen Graf and Christoph Scheben},
title = {A Hybrid Approach for Proving Noninterference and
Applications to the Cryptographic Verification of {Java}
Programs},
booktitle = {Grande Region Security and Reliability Day 2013},
url = {http://grsrd.uni.lu/papers/grsrd2013_submission_2.pdf},
year = 2013,
editor = {Christian Hammer and Sjouke Mauw},
address = {Luxembourg},
note = {Extended Abstract}
}
@inproceedings{KlebanovMM13,
author = {Vladimir Klebanov and Norbert Manthey and Christian Muise},
title = {{SAT}-based Analysis and Quantification of Information Flow in Programs},
booktitle = {Proceedings, International Conference on Quantitative
Evaluation of Systems (QEST)},
year = {2013},
publisher = {Springer},
series = {LNCS},
volume = {8054},
pages = {156-171},
doi = {10.1007/978-3-642-40196-1_16},
url = {http://formal.iti.kit.edu/~klebanov/pubs/qest2013.pdf}
}
@inproceedings{SchebenSchmitt14,
author = {Christoph Scheben and Schmitt, Peter H.},
title = {Efficient Self-Composition for Weakest Precondition Calculi},
booktitle = {Proceedings, 19th International Symposium on Formal Methods (FM)},
year = {2014},
volume = {8442},
series = {LNCS},
editor = {Jones, Cliff and Pihlajasaari, Pekka and Sun, Jun},
doi = {10.1007/978-3-319-06410-9_39},
publisher = {Springer International Publishing},
pages = {579-594}
}
@article{Klebanov14,
author = {Vladimir Klebanov},
title = {Precise Quantitative Information Flow Analysis -- A Symbolic Approach},
year = {2014},
journal = {Theoretical Computer Science},
volume = {538},
number = {0},
pages = {124-139},
doi = {10.1016/j.tcs.2014.04.022}
}
@inproceedings{DoerreKlebanov16a,
author = {Felix D{\"o}rre and Vladimir Klebanov},
title = {Practical Detection of Entropy Loss in Pseudo-Random Number Generators},
booktitle = {Proceedings, ACM Conference on Computer and Communications Security (CCS)},
year = 2016
}
@inproceedings{KlebanovWW16,
author = {Vladimir Klebanov and Alexander Weigl and J{\"o}rg Weisbarth},
title = {Sound Probabilistic #SAT with Projection},
booktitle = {Proceedings, Workshop on Quantitative Aspects of Programming Languages and Systems (QAPL)},
year = 2016
}
@inproceedings{QASA2016,
author = {Alexander Weigl},
title = {Efficient {SAT}-based Pre-image Enumeration for Quantitative Information Flow in Programs},
booktitle = {5th International Workshop on Quantitative Aspects of Security Assurance (QASA 2016)},
year = 2016
}
@inproceedings{BeckertBischofEA2017,
author = {Bernhard Beckert and Simon Bischof
and Mihai Herda and Michael Kirsten
and Marko {Kleine B\"{u}ning}},
title = {Combining Graph-Based and Deduction-Based Information-Flow Analysis},
booktitle = {5th Workshop on Hot Issues in Security Principles and Trust (HotSpot 2017)
affiliated with ETAPS 2017: European Joint Conferences on Theory and
Practice of Software},
url = {https://sec.informatik.uni-stuttgart.de/_media/events/hotspot2017/proceedings.pdf},
month = apr,
year = {2017},
abstract = {Information flow control (IFC) is a category of techniques for ensuring system
security by enforcing information flow properties such as non-interference.
Established IFC techniques range from fully automatic approaches with much
over-approximation to approaches with high precision but potentially laborious
user interaction. A noteworthy approach mitigating the weaknesses of both
automatic and interactive IFC techniques is the hybrid approach, developed by
K\"{u}sters et al., which -- however -- is based on program modifications and
still requires a significant amount of user interaction.
\newline
In this paper, we present a combined approach that works without any program
modifications. It minimizes potential user interactions by applying a
dependency-graph-based information-flow analysis first. Based on
over-approximations, this step potentially generates false positives. Precise
non-interference proofs are achieved by applying a deductive theorem prover with
a specialized information-flow calculus for checking that no path from a secret
input to a public output exists. Both tools are fully integrated into a combined
approach, which is evaluated on a case study, demonstrating the feasibility of
automatic and precise non-interference proofs for complex programs.},
place = {Uppsala, Sweden},
date = {April 23}
}
@phdthesis{Grahl15,
author = {Daniel Grahl},
title = {Deductive Verification of Concurrent Programs and its
Application to Secure Information Flow for {Java}},
school = {Karlsruhe Institute of Technology},
year = 2015,
month = {29~} # oct,
url = {https://digbib.bibliothek.kit.edu/volltexte/1000050695},
urn = {urn:nbn:de:swb:90-506951},
doi = {10.5445/IR/1000050695},
abstract = {The goal of this thesis is to develop a rigorous analysis
technique for proving functional and relational correctness
of shared-memory multi-threaded object-oriented software
systems---such as programs written in the Java
language---based on formal program semantics and deductive
verification. This work contains the first approach towards
a semantically precise information flow anlaysis for
concurrent programs.}
}
@techreport{Bruns15,
author = {Bruns, Daniel},
title = {Deductive Verification of Concurrent Programs},
year = 2015,
institution = {Department of Informatics, Karlsruhe Institute of
Technology},
number = {2015-3},
series = {Karlsruhe Reports in Informatics},
url = {https://digbib.bibliothek.kit.edu/volltexte/1000045641},
urn = {urn:nbn:de:swb:90-456415},
issn = {2190-4782},
license = {http://creativecommons.org/licenses/by-nc-nd/3.0/},
abstract = {Verification of concurrent programs still poses one of the
major challenges in computer science. Several techniques to
tackle this problem have been proposed. However, they often
do not scale. We present an adaptation of the rely\slash
guarantee methodology in dynamic logic. Rely\slash
guarantee uses functional specification to symbolically
describe the behavior of concurrently running threads:
while each thread \emph{guarantees} adherence to a
specified property at any point in time, all other threads
can \emph{rely} on this property being established. This
allows to regard threads largely in isolation---only
w.r.t.\ an environment constrained by these specifications.
While rely\slash guarantee based approaches often suffer
from a considerable specification overhead, we complement
functional thread specifications with frame conditions.
We will explain our approach using a simple, but concurrent
programing language. Besides the usual constructs for
sequential programs, it caters for dynamic thread creation.
We define semantics of concurrent programs w.r.t.\ an
underspecified deterministic scheduling function.
To formally reason about programs of this language, we
introduce a novel multi-modal logic, \emph{Concurrent
Dynamic Trace Logic} (CDTL). It combines the strengthes of
dynamic logic with those of linear temporal logic and
allows to express temporal properties about symbolic
program traces. We first develop a sound and complete
sequent calculus for the logic subset that uses the
sequential part of the language, based on symbolic
execution. In a second step, we extend this to a calculus
for the complete logic by adding symbolic execution rules
for concurrent interleavings and dynamic thread creation
based on the rely\slash guarantee methodology. Again, this
calculus is proven sound and complete. }
}
@phdthesis{Scheben14,
author = {Christoph Scheben},
title = {Program-level Specification and Deductive Verification of
Security Properties},
year = 2014,
school = {Karlsruhe Institute of Technology},
url = {https://digbib.bibliothek.kit.edu/volltexte/1000046878}
}
@mastersthesis{Nikolov14,
author = {Pavel Nikolov},
title = {Combining theorem proving and type systems for precise
and efficient information flow verification},
type = {Studienarbeit},
school = {Karlsruhe Institute of Technology},
year = 2014
}
@mastersthesis{Wagner13,
author = {Andreas Wagner},
title = {Trace Based Reasoning with {KeY} and {JML}},
year = 2013,
school = {Karlsruhe Institute of Technology},
type = {Studienarbeit},
url = {https://www.key-project.org/DeduSec/2013_Wagner_TraceSpecification.pdf}
}
@mastersthesis{Ruch13,
author = {Fabian Ruch},
title = {Efficient Logic-Based Information Flow Analysis Of
Object-Oriented Programs},
year = 2013,
type = {Bachelor thesis},
school = {Karlsruhe Institute of Technology},
url = {https://digbib.bibliothek.kit.edu/volltexte/1000036850},
urn = {urn:nbn:de:swb:90-368506}
}
@mastersthesis{Wallisch14,
author = {Kai Wallisch},
title = {Maps in {Java} Dynamic Logic},
type = {Studienarbeit},
year = 2014,
school = {Karlsruhe Institute of Technology}
}
@techreport{Bruns14a,
author = {Bruns, Daniel},
title = {Formal Verification of an Electronic Voting System},
year = 2014,
institution = {Department of Informatics, Karlsruhe Institute of
Technology},
number = {2014-11},
series = {Karlsruhe Reports in Informatics},
url = {https://digbib.bibliothek.kit.edu/volltexte/1000042284},
urn = {urn:nbn:de:swb:90-422842},
issn = {2190-4782},
license = {http://creativecommons.org/licenses/by-nc-nd/3.0/},
abstract = {Electronic voting (e-voting) systems that are used in
public elections need to fulfil a broad range of strong
requirements concerning both safety and security. Among
these requirements are reliability, robustness, privacy of
votes, coercion resistance and universal verifiability.
Bugs in or manipulations of an e-voting system may have
considerable influence on the life of the humans living in
a country where such a system is used. Hence, e-voting
systems are an obvious target for software verification.
In this paper, we report on an implementation of such a
system in Java and the formal verification of functional
properties thereof in the \KeY verification system. Even
though the actual components are clearly modularized, the
challenge lies in the fact that we need to prove a highly
nonlocal property: After all voters have cast their votes,
the server calculates the correct votes for each candidate
w.r.t.\ the original ballots. This kind of trace property
is difficult to prove with static techniques like
verification and typically yields a large specification
overhead. }
}
@techreport{Bruns14b,
author = {Daniel Bruns},
title = {Towards Specification and Verification of Information Flow
in Concurrent {Java-}like Programs},
year = 2014,
institution = {Department of Informatics, Karlsruhe Institute of
Technology},
number = {2014-5},
series = {Karlsruhe Reports in Informatics},
url = {https://digbib.bibliothek.kit.edu/volltexte/1000039446},
urn = {urn:nbn:de:swb:90-394465},
license = {http://creativecommons.org/licenses/by-nc-nd/3.0/}
}
@techreport{BeckertBrunsKlebanovEtAl13,
author = {Bernhard Beckert and Daniel Bruns and Vladimir Klebanov
and Christoph Scheben and Peter H. Schmitt and Mattias
Ulbrich },
title = {Information Flow in Object-Oriented Software -- Extended
Version --},
year = 2013,
institution = {Department of Informatics, Karlsruhe Institute of
Technology},
number = {2013-14},
series = {Karlsruhe Reports in Informatics},
license = {http://creativecommons.org/licenses/by-nc-nd/3.0/},
url = {https://digbib.bibliothek.kit.edu/volltexte/1000037606},
urn = {urn:nbn:de:swb:90-376067},
issn = {2190-4782}
}
@techreport{beckert.bruns12b,
author = {Bernhard Beckert and Daniel Bruns},
title = {Dynamic Trace Logic: Definition and Proofs},
year = 2012,
institution = {Department of Informatics, Karlsruhe Institute of
Technology},
number = {2012-10},
series = {Karlsruhe Reports in Informatics},
url = {https://digbib.bibliothek.kit.edu/volltexte/1000028184},
urn = {urn:nbn:de:swb:90-281845},
license = {http://creativecommons.org/licenses/by-nc-nd/3.0/de},
abstract = { Dynamic logic is an established instrument for program
verification and for reasoning about the semantics of
programs and programming languages. In this paper, we
define an extension of dynamic logic, called Dynamic Trace
Logic~(DTL), which combines the expressiveness of program
logics such as dynamic logic with that of temporal logic.
And we present a sound and relatively complete sequent
calculus for proving validity of DTL formulae. Due to its
expressiveness, DTL can serve as a basis for functional
verification of concurrent programs and for proving
information-flow properties among other applications.}
}
@techreport{beckert.bruns.ea12b,
author = {Bernhard Beckert and Daniel Bruns and Ralf K\"{u}sters and
Christoph Scheben and Schmitt, Peter H. and Tomasz
Truderung},
title = {The {KeY} Approach for the Cryptographic Verification of
{J}ava Programs: {A} Case Study},
institution = {Department of Informatics, Karlsruhe Institute of
Technology},
number = {2012-8},
year = {2012},
series = {Karlsruhe Reports in Informatics},
url = {https://digbib.bibliothek.kit.edu/volltexte/1000027497},
urn = {urn:nbn:de:swb:90-274973},
license = {http://creativecommons.org/licenses/by-nc-nd/3.0/de},
abstract = { In this paper, we report on an ongoing case study in
which we use the KeY tool, a theorem prover for checking
functional correctness and noninterference properties of
Java programs, to establish computational
indistinguishability for a simple Java program that
involves clients sending encrypted messages over an
untrusted network to a server. The analysis uses a general
framework, recently proposed by K{\"u}sters et al., which
enables program analysis tools, such as KeY, that can
check (standard) noninterference properties for Java
programs to establish computational indistinguishability
properties. }
}
@misc{DoerreKlebanov16b,
author = {Felix D{\"o}rre and Vladimir Klebanov},
title = {Entropy Loss and Output Predictability in the Libgcrypt PRNG (CVE-2016-6313)},
year = 2016,
url = {http://formal.iti.kit.edu/~klebanov/libgcrypt-cve-2016-6313.pdf}
}
This file was generated by bibtex2html 1.97.