Invited Speakers
Martin Abadi, Microsoft Research Silicon Valley and UC Santa Cruz
Software Security: A Formal Perspective
Abstract. Weaknesses in software security have been numerous, sometimes startling, and often serious. Many of them stem from apparently small low-level errors (e.g., buffer overflows). Ideally, those errors should be avoided by design, or at least fixed after the fact. In practice, on the other hand, we may have to tolerate some vulnerabilities, with appropriate models, architectures, and tools. This short paper is intended to accompany a talk at the 18th International Symposium on Formal Methods (FM 2012). The talk will discuss software security with an emphasis on low-level attacks and defenses and on their formal aspects. It will focus on systematic mitigations (specifically, techniques for layout randomization and control-flow integrity) that aim to be effective in the presence of buggy software and powerful attackers.
Asaf Degani, General Motors
Formal Methods in the Wild: Trains, Planes and Automobile
Abstract. Why is it that carefully researched and well-formulated theoretical and methodological constructs don't make their way into industrial applications? This keynote speech takes a look at my personal experiences in both the aviation and automotive fields to suggest what can be done about it. I will first try to explain why engineers (and even industry scientists) tend not to use the kind of methods and tools that emerge from academic settings while working on actual products, and then show some of the consequences of not using such methods. I will end with a few vignettes from my own trials and tribulations in applying formal methods in engineering design processes as well as some of the future prospects, for both academia and industry, as human-automation systems become more demanding and complex.
Alan Wassyng, McMaster Centre for Software Certi cation, Department of Computing and Software, McMaster University, Hamilton, Ontario, Canada
Who are we, and what are we doing here?
Abstract. Many Formal Methods researchers and practitioners seem to treat Formal Methods more as a religion than as an approach to rigorous software engineering. This fervour has a few side-e ects: i) There have been spectacular advances in a few areas in Formal Methods; ii) There are a signi cant number of highly e ective Formal Methods advocates and practitioners; iii) The Formal Methods community at large seems to be condescendingly dismissive of any protestation of disbelief; and iv) Different methods and approaches seem to be judged on a belief basis rather than through evidence based analysis. The essential fact remains though, that after decades of research, Formal Methods are not used much in industrial software development. It is time that we, the Formal Methods community, question the basis of our existence.