[Busec] group meeting next week - Mark Renyolds

Sharon Goldberg goldbe at cs.bu.edu
Fri Oct 14 16:11:44 EDT 2011


At Monday's group meeting we'll have a talk by Mark Renyolds.  1PM,
MCS137, and lunch will be provided.

See you then!

Verification of Security and Scheduling Properties using Lightweight
Formal Methods

Mark Reynolds
Boston University

 A property is a constraint that well-formed code must satisfy. In a
security context, properties might include ‚ uninitialized memory is
never read‚ and the target of a transfer of control is always the
beginning of an instruction. In a scheduling or OS context, properties
might include, under certain (stated) assumptions resource deadlocks
never occur‚ and in the fair scheduler, no process or thread is ever
blocked indefinitely. Formal verification of such properties is often
very difficult. This talk describes the use of the lightweight
modeling language Alloy as a tool for providing for property
verification. Alloy is not a proof system, it is a counterexample
system. If an Alloy model exposes a counterexample to a stated
property, then it must represent a flaw in the system being modeled,
such as security vulnerability. If the model does not exhibit any
counterexamples, this is not a proof that the property is always
satisfied; instead, it is an assertion that within the search scope of
the model analyzer, the property is satisfied. This approach has
proven to be an extremely useful tool in discovering security
vulnerabilities as well as deficiencies in resource and scheduling

(This talk will cover part of the research conducted by Mark Reynolds
for his doctoral thesis.)

Sharon Goldberg
Computer Science, Boston University

More information about the Busec mailing list