The Verifying Compiler: still a Grand Challenge for
I propose a set of criteria which distinguish a grand
challenge in science or engineering from the many other kinds of
short-term or long-term research problems that engage the interest of
scientists and engineers. As an example drawn from Computer Science, I
revive an old challenge: the construction and application of a verifying
compiler that guarantees correctness of a program before running it.
Computer Security from a Programming Language and
Static Analysis Perspective.
This talk outlines the role of languages, static analyses and
semantics in the general issue of building secure computer systems.
In particular, I will discuss the use of static typing and other
static analyses for implementing access control policies. Next, I
will show how these ideas impact the programming of smart cards.
, Naval Research Laboratory, USA
What Makes a Cryptographic Protocol Secure?
The Evolution of Requirements Specification in Formal
Cryptographic Protocol Analysis.
Much attention has been paid to the design of languages for the
specification of cryptographic protocols. However, the ability to specify
their desired behavior correctly is also important; indeed many perceived
protocol flaws arise out of a misunderstanding of the protocol's
requirements. In this talk we give a brief survey of the history
of requirements specification in formal analysis of cryptographic protocols.
We outline the main approaches and describe some of the open
Dimensions of Precision in Reference Analysis
of Object-oriented Programming Languages
There has been approximately a ten year history of reference analyses
for object-oriented programming languages. Approaches vary as to how
different analyses account for program execution flow, how they capture
calling context, and how they model objects, reference variables and the
possible calling structure of the program. A taxonomy of analysis
dimensions that affect precision (and cost) will be presented and
illustrated by examples of existing reference analysis techniques.