<html><head><style type='text/css'>p { margin: 0; }</style></head><body><div style='font-family: arial,helvetica,sans-serif; font-size: 12pt; color: #000000'><b>What are the Right Roles for Formal Methods in High Assurance Cloud Computing?</b>
<br>
<b><a href="http://www.cs.cornell.edu/ken/">Ken Birman</a></b>, <a href="http://www.cs.cornell.edu/">Cornell University</a>
<br>Tuesday, November 13, 2012- 4:30pm<br>Computer Science 105<br>
<br>
The developer of a high assurance system must justify the fitness of the
system for the intended use. In "small" scenarios, this problem is well
understood: it entails rigorously specifying properties the system must
achieve, designing protocols and correctness proofs, and then
implementing and testing the needed code. In scaled-out settings,
complex architectures are often unavoidable and this methodology can no
longer be used.<br><br><p>
This talk focuses on how the resulting problems play out in the context
of Isis2 (isis2.codeplex.com), a new system I've been building that
supports a wide range of high-assurance properties for applications that
will be hosted on cloud computing datacenters, and hence might need to
run at very ambitious scale. <br></p><p><br></p><p>
We'll see that while it is possible to create systems of these kinds,
existing formal methods are ill-suited to reasoning about the resulting
solutions, suggesting that additional work will be needed to bridge
between the mathematical and scientific foundations of high assurance of
the kinds we teach in academic settings and the real-world instances of
such problems that we may face in the near future. <br></p><p><br></p>
Ken Birman is the N. Rama Rao Professor of Computer Science at
Cornell University, where he has headed a research effort in the area of
high assurance distributed computing for thirty years. Ken is best
known for inventing the virtual synchrony computing model and building
the Isis Toolkit, which was ultimately used to build the system that
operated the New York Stock Exchange for more than a decade, and the
systems that continue to operate the French Air Traffic Control system
and the US Navy AEGIS today. He also pioneered in the use of gossip
protocols for system monitoring, management and control; several of his
solutions are used today in the platforms that operate today's largest
cloud computing infrastructures, notably at Amazon, IBM and Microsoft.
A Fellow of the ACM since 1999, Ken won the 2009 IEEE Kanai Award for
his research in distributed systems. He is currently developing online
instructional materials for a short course on building high assurance
cloud computing systems using his Isis2 platform.
</div></body></html>