Seminar by Dr Apu Kapadia, Indiana University

We introduce Soundcomber, a “sensory malware” for smartphones that
uses the microphone to steal private information from phone
conversations. Soundcomber is lightweight and stealthy. It uses
targeted profiles to locally analyze portions of speech likely to
contain information such as credit card numbers. It evades known
defenses by transferring small amounts of private data to the malware
server utilizing smartphone-specific covert channels. Additionally, we
present a general defensive architecture that prevents such sensory
malware attacks.

Systems Seminar – by John Thomson

All wecome.

The Results Delusion

Abstract:

It is often said that any subject which requires the word ‘science’ to be placed somewhere in its name, is unlikely to be very scientific. This is unfortunately far too true for systems research in general. Every systems conference, papers are presented which show significant speedups over previous approaches to problem X, but these improvements are rarely replicated in output from industry. Why? The unpalatable answer is that a significant amount of systems research is the result of self-delusion, bad science and, I suspect occasionally, fraud.

Standards of scientific rigour in CS often fall well below what would be taken for granted in other sciences – particularly with regard to measurement of results, statistical analysis and replicability of results. I would like to do something about this, and will be presenting the idea for a new CS journal, which focuses on this exact problem. Oh, and peer review is gone too! Pitfalls abound. Would love to hear your comments, objections and advice.

Thirty five years ago computers made a dramatic debut in mathematics with the famous proof of the Four Color Theorem by Appel and Haken. Their role has been expanding recently, from computational devices to tools that can tackle deduction and proofs too complex for (most) human minds, such as the Kepler conjecture or the Classification of Finite Simple Groups.

 These new “machine” proofs entail fundamental changes in the practice of mathematics: a shift from craftsmanship, where each argument is a tribute to the ingenuity of the mathematician that perfected it, to a form of engineering where proofs are created more systematically. In addition to formal definitions and theorems, mathematical theories also contain clever, context-sensitive notations, usage conventions, and proof methods. To mechanize advanced mathematical results it is essential to capture these more informal elements, replacing informal and flexible usage conventions with rigorous interfaces, and exercise apprenticeship with precise algorithms. This can be difficult, requiring an array of techniques closer to software engineering than formal logic, but it is essential to obtaining formal proofs of graduate-level mathematics, and can give new insight as well.

 In this talk we will give several examples of such empirical formal mathematics that we have encountered in the process of mechanizing a large corpus of Combinatorics and Algebra required by the proofs of the Four Colour and Odd Order Theorem.

 Bio:Georges Gonthier is a Principal Researcher at Microsoft Research Cambridge. Dr. Gonthier has worked on the Esterel reactive programming language, techniques for the optimal computation of functional programs, the design and formal verification of a concurrent garbage collector, the join calculus model of concurrency, concurrency analysis of the Ariane 5 flight software, using full abstraction in the analysis of security properties, and a fully computer-checked proof of the famous Four Colour Theorem. He now heads the Mathematical Components project at the MSR Inria Joint Center, following up on the latter work with the development of a comprehensive library of formalized abstract algebra.

Georges Gonthier – Head of the Mathematical Components team Microsoft Research-INRIA joint centre http://www.msr-inria.inria.fr/

There will be bisquits from 3:45 downstairs