Room 4.03, Appleton Tower, University of Edinburgh
This meeting of the Scottish Theorem Proving seminar has been organised by Graham Steel. Please contact Graham Steel for further details or clarification.
Travel information, maps etc. can be found here.
More information about Scottish Theorem Proving can be found here.
Abstract
A hardware security module, or HSM, is a tamper-proof piece of computer hardware used to carry out a small set of cryptographic operations. HSMs are used in various security-critical applications such as banking systems, electronic payment devices and cash machines (ATMs). Typically, such devices have a restricted application program interface (API) that prescribes how an application program can make requests of the module to carry out commands. Various attacks have been found on these APIs in recent times by a combination of 'by-hand' analysis and ad-hoc formal methods. We are just starting work on a project to develop more generic formal tools for analysing these APIs. This talk will introduce APIs, give some examples of attacks, and some ideas we have about how their analysis might be formalised.
Abstract
High integrity software systems call for various levels of static analysis. Hume is a functional programming language, targeted at safety-critical systems, which supports static analysis for time and space. However, formal verification is not part of the current Hume static analysis tool set. This gap is addressed by exploring the use of Hume with an off-the-shelf design verification system called Spin. The rules for translating a subset of Hume into the notation required by Spin are investigated. An empirical analysis targeted at the translation and verification of the translated programs is conducted.
Abstract
There are several automated systems capable of generating, in certain mathematical domains, thousands upon thousands of true statements -- "theorems", from a logical point of view. However, most likely, only a small handful of these statements would be considered "theorems", from a mathematical point of view. We describe our approach, from a work in progress, to distinguish between those true statements which mathematicians would deem worthy of the name "Theorem", and those which they would not. We also present a brief demonstration of the system we are developing, which implements this approach.
