Ronitt Rubinfeld
(MIT), Something for Almost Nothing: Advances in Sublinear Time Algorithms
Lineartime algorithms have long been considered the gold
standard of computational endciency. Indeed, it is hard to imagine doing
better than that, since for a nontrivial problem, any algorithm must
consider all of the input in order to make a decision. However, as extremely
large data sets are pervasive, it is natural to wonder what one
can do in sublinear time. Over the past two decades, several surprising
advances have been made on designing such algorithms. We will give a
nonexhaustive survey of this emerging area, highlighting recent progress
and directions for further research.
Gilles Barthe
(IMDEA Software Institute), ComputerAided Cryptographic Proofs
EasyCrypt [6] is a computerassisted
framework for reasoning about the security of cryptographic
constructions, using the methods and tools of provable security, and
more specifically of the gamebased techniques. The core of
EasyCrypt is a relational program logic for a core
probabilistic programming language with sequential composition,
conditionals, loops, procedure calls, assignments and sampling from
discrete distributions. The relational program logic is key to capture
reductionist arguments that arise in cryptographic proofs. It is
complemented by a (standard, nonrelational) program logic that allows
to reason about the probability of events in the execution of
probabilistic programs; this program logic allows for instance to
upper bound the probability of failure events, that are pervasive in
gamebased cryptographic proofs. In combination, these logics capture
general reasoning principles in cryptography and have been used to
verify the security of emblematic constructions, including the
FullDomain Hash signature [8],
the Optimal Asymmetric Encryption
Padding (OAEP) [7], hash
function designs [3] and zeroknowledge
protocols [5, 1].
Yet, these logics can only capture instances of
general principles, and lack mechanisms for stating and proving these
general principles once and for all, and then for instantiating them
as needed. To overcome this limitation, we have recently
extended EasyCrypt with programming language mechanisms
such as modules and type classes. Modules provide support for
composition of cryptographic proofs, and for formalizing hybrid
arguments, whereas type classes are convenient to model and reason
about algebraic structures. Together, these extensions significantly
expand the class of examples that can be addressed
with EasyCrypt . For instance, we have used the latest
version of EasyCrypt to verify the security of a class of
authenticated key exchange protocols, and of a secure function
evaluation protocol based on garbled circuits and oblivious transfer.
Our current work explores two complementary directions. On the one
hand, we are extending the EasyCrypt infrastructure in
order to derive security guarantees about implementations of
cryptographic constructions. Indeed, practical attacks often target
specific implementations and exploit some characteristics that are not
considered in typical provable security proofs; as a consequence,
several widely used implementations of provably secure schemes are
vulnerable to attacks. In order to narrow the gap between provable
security and implementations, we are extending EasyCrypt
with support to reason about Clike implementations, and use the
CompCert verified C compiler
(http://compcert.inria.fr) to
carry the security guarantees down to executable implementations
[2]. On the other hand, we are developing specialized formalisms to
reason about the security of particular classes of constructions. For
instance, we have recently developed the ZooCrypt framework [4], which
supports automated analysis of chosenplaintext and chosen
ciphertextsecurity for publickey encryption schemes built from
(partialdomain) oneway trapdoor permutations and random
oracles. Using ZooCrypt , we have analyzed over a million
(automatically generated) schemes, including many schemes from the
literature. For chosenplaintext security, ZooCrypt is able to report
in nearly 99% of the cases a proof of security with a concrete
security bound, or an attack. We are currently extending our approach
to reason about encryption schemes based on DiffieHellmann groups and
bilinear pairings, both in the random oracle and in the standard
models. More information about the project is available from the
project web page
http://www.easycrypt.info.
References
1. Almeida, J.B., Barbosa, M., Bangerter, E., Barthe,
G., Krenn, S., ZanellaBé́guelin, S.: Full proof cryptography:
verifiable compilation of efficient zeroknowledge protocols. In: 19th
ACM Conference on Computer and Communications Security. ACM (2012)
2. Almeida, J.B., Barbosa, M., Barthe, G., Dupressoir,
F.: Certified computeraided cryptography: efficient provably secure
machine code from highlevel implementations. In: ACM Conference on
Computer and Communications Security. ACM (2013)
3. Backes, M., Barthe, G., Berg, M., Grégoire,
B., Skoruppa, M., ZanellaBéguelin, S.: Verified security of
MerkleDamgård. In: IEEE Computer Security Foundations. ACM
(2012)
4. Barthe, G., Crespo, J.M., Grégoire, B., Kunz,
C., Lakhnech, Y., Schmidt, B., ZanellaBéguelin, S.: Automated
analysis and synthesis of paddingbased encryption schemes. In: ACM
Conference on Computer and Communications Security. ACM (2013)
5. Barthe, G., Grégoire, B., Hedin, D., Heraud,
S., ZanellaBéguelin, S.: A MachineChecked Formalization of
SigmaProtocols. In: IEEE Computer Security Foundations. ACM (2010)
6. Barthe, G., Grégoire, B., Heraud, S.,
ZanellaBéguelin, S.: Computeraided security proofs for the
working cryptographer. In: Rogaway, P. (ed.) CRYPTO 2011. LNCS,
vol. 6841, pp. 71–90. Springer, Heidelberg (2011)
7. Barthe, G., Grégoire, B., Lakhnech, Y.,
ZanellaBéguelin, S.: Beyond Provable Security Verifiable
INDCCA Security of OAEP. In: Kiayias, A. (ed.) CTRSA 2011. LNCS,
vol. 6558, pp. 180–196. Springer, Heidelberg (2011)
8. ZanellaBéguelin, S., Barthe, G.,
Grégoire, B., Olmedo, F.: Formally certifying the security of
digital signature schemes. In: IEEE Symposium on Security and Privacy.
IEEE Computer Society (2009)
Robert Sedgewick
(Princeton), “If You Can Specify It, You Can Analyze It” — The Lasting Legacy of Philippe Flajolet
The “Flajolet School” of the analysis of algorithms and combinatorial
structures is centered on an effective calculus, known as analytic
combinatorics, for the development of mathematical models that are
sufficiently accurate and precise that they can be validated through
scientific experimentation. It is based on the generating function as
the central object of study, first as a formal object that can
translate a specification into mathematical equations, then as an
analytic object whose properties as a function in the complex plane
yield the desired quantitative results. Universal laws of sweeping
generality can be proven within the framework, and easily
applied. Standing on the shoulders of Cauchy, Polya, de Bruijn, Knuth,
and many others, Philippe Flajolet and scores of collaborators
developed this theory and demonstrated its effectiveness in a broad
range of scientific applications. Flajolet's legacy is a vibrant field
of research that holds the key not just to understanding the
properties of algorithms and data structures, but also to
understanding the properties of discrete structures that arise as
models in all fields of science. This talk will survey Flajolet's
story and its implications for future research.
“A man … endowed with an an exuberance of imagination which puts
it in his power to establish and populate a universe of his own creation”.
Gonzalo Navarro
(University of Chile), Encoding Data Structures
Classical data structures can be regarded as additional information
that is stored on top of the raw data in order to speed up some kind
of queries. Some examples are the suffix tree to support pattern
matching in a text, the extra structures to support lowest common
ancestor queries on a tree, or precomputed shortest path information
on a graph.
Some data structures, however, can operate without accessing the
raw data. These are called encodings. Encodings are relevant when
they do not contain enough information to reproduce the raw data, but
just what is necessary to answer the desired queries (otherwise, any
data structure could be seen as an encoding, by storing a copy of the
raw data inside the structure).
Encodings are interesting because they can occupy much less space
than the raw data. In some cases the data itself is not interesting,
only the answers to the queries on it, and thus we can simply discard
the raw data and retain the encoding. In other cases, the data is used
only sporadically and can be maintained in secondary storage, while
the encoding is maintained in main memory, thus speeding up the most
relevant queries.
When the raw data is available, any computable query on it can be
answered with sufficient time. With encodings, instead, one faces a
novel fundamental question: what is the effective entropy of the data
with respect to a set of queries? That is, what is the minimum size
of an encoding that can answer those queries without accessing the
data? This question is related to Information Theory, but in a way
inextricably associated to the data structure: the point is not how
much information the data contains, but how much information is
conveyed by the queries. In addition, as usual, there is the issue of
how efficiently can be the queries answered depending on how much
space is used.
In this talk I will survey some classical and new encodings,
generally about preprocessing arrays \(A[1, n]\) so as to answer
queries on array intervals \([i, j]\) given at query time. I will
start with the classical range minimum queries (which is the minimum
value in \(A[i,j]\)?) which has a long history that culminated a
few years ago in an asymptotically spaceoptimal encoding of
\(2n+o(n)\) bits answering queries in constant time. Then I will
describe more recent (and partly open) problems such as finding the
second minimum in \(A[i, j]\), the \(k\) smallest values in
\(A[i, j]\), the \(k\)th smallest value in \(A[i, j]\), the elements
that appear more than a fraction τ of the times in \(A[i, j]\),
etc. All these queries appear recurrently within other algorithmic
problems, and they have also direct application in data mining.
J. Ian Munro
(University of Waterloo), Succint Data Structures ... Not Just for Graphs
Succinct data structures are data representations that use
(nearly) the information theoretic minimum space, for the combinatorial
object they represent, while performing the necessary query operations
in constant (or nearly constant) time. So, for example, we can
represent a binary tree on n nodes in \(2n + o(n)\) bits, rather than the
“obvious” \(5n\) or so words, i.e. \(5n \lg(n)\) bits. Such a difference in memory
requirements can easily translate to major differences in runtime as a
consequence of the level of memory in which most of the data resides.
The field developed to a large extent because of applications in text indexing,
so there has been a major emphasis on trees and a secondary
emphasis on graphs in general; but in this talk we will draw attention to
a much broader collection of combinatorial structures for which succinct
structures have been developed. These will include sets, permutations,
functions, partial orders and groups, and yes, a bit on graphs.
