Thursday, Oct 8, 2009
4:30 PM - 5:30 PM
5331 CS
|
Cynthia Sturton, Susmit Jha, David Wagner and Sanjit
Seshia
On Voting Machine Design for Verification and Testability
Download paper
We present an approach for the design and analysis of an electronic
voting machine based on a novel combination of formal verification
and systematic testing. The system was designed specifically
to enable verification and testing. In our architecture, the voting
machine is a finite-state transducer that implements the bare essentials
required for an election. We formally specify how each
component of the machine is intended to work and formally verify
that a Verilog implementation of our design meets this specification.
However, it is more challenging to verify that the composition
of these components will behave as a voter would expect, because
formalizing human expectations is difficult. We show how systematic
testing can be used to address this issue, and in particular to
verify that the machine will behave correctly on election day.
|
Thursday, Oct 29, 2009
4:30 PM - 5:30 PM
3310 CS
|
Roxana Geambasu, Tadayoshi Kohno, Amit A. Levy, and Henry M. Levy
Vanish: Increasing Data Privacy with Self-Destructing Data
Download Paper
Today's technical and legal landscape presents
formidable challenges to personal data privacy. First,
our increasing reliance on Web services causes personal
data to be cached, copied, and archived by third parties,
often without our knowledge or control. Second, the
disclosure of private data has become commonplace due
to carelessness, theft, or legal actions.
Our research seeks to protect the privacy of past,
archived data -- such as copies of emails maintained
by an email provider -- against accidental, malicious,
and legal attacks. Specifically, we wish to ensure that
all copies of certain data become unreadable after a user-specified
time, without any specific action on the part of
a user, and even if an attacker obtains both a cached copy
of that data and the user's cryptographic keys and passwords.
This paper presents Vanish, a system that meets this
challenge through a novel integration of cryptographic
techniques with global-scale, P2P, distributed hash tables
(DHTs). We implemented a proof-of-concept Vanish
prototype to use both the million-plus-node Vuze Bit-
Torrent DHT and the restricted-membership OpenDHT.
We evaluate experimentally and analytically the functionality,
security, and performance properties of Vanish,
demonstrating that it is practical to use and meets the
privacy-preserving goals described above. We also describe
two applications that we prototyped on Vanish: a
Firefox plugin for Gmail and other Web sites and a Vanishing
File application.
Note: An independent group of researchers have
published an attack on this system. Their writeup can
be found here.
|