quick.links

recent.news

2009-12-18 - The slides from my recent presentation at CRESTCon 2009, the 'replacement' for CHECKCon, are now online! exploit code for the demonstrations [...]

2009-03-30 - We (by we, I mean myself and christer) recently demonstrated a score of local (and indeed a remote) kernel vulnerabilities [...]

:.home.research3.14159..

basic research is what I am doing when I don't know what I am doing.

pub.lications

  • September 02-08
    - Anytime Algorithms for ROBDD Symmetry Detection and Approximation
    Neil Kettle
    PhD thesis, Computing Laboratory, University of Kent, Canterbury, Kent, CT2 7NF.
    [ thesis (pdf) - abstract ]
  • June 17-08
    - Bit-Precise Reasoning with Affine Functions
    Neil Kettle and Andy King
    In 1st International Workshop on Bit-Precise Reasoning (BPR-2008)
    Abstract: The class of affine Boolean functions is rich enough to express constant bits and dependencies between different bits of different words. For example, the function $(x_0)wedge(¬y_1)wedge(x_4 iff y_7)wedge(x_5 iff ¬y_9)$ is affine and expresses the invariant that the low bit (bit $0$) of the variable $x$ is true, that bit $1$ of $y$ is false, that the bits $4$ and $7$ of $x$ and $y$ coincide whereas bits $5$ and $9$ of $x$ and $y$ differ. This class of Boolean function is amenable to bit-precise reasoning since it satisfies strong chain properties which bound the number of times a system of semantic fixpoint equations need to be reapplied when reasoning about loops. This paper address the key problem of abstracting an arbitrary Boolean function to either a general affine function or a so-called affine function of width 2, when the function is represented as an ROBDD. Novel algorithms are presented for this task: one that manipulates Boolean vectors and another which is inspired by anti-unification. The speed and precision of both algorithms are compared on benchmark circuits, to draw conclusions on the tractability of affine abstraction.
    [ paper (pdf) - link - no abstract ]
  • August 30-07
    - An Anytime Algorithm for Generalized Symmetry Detection in ROBDDs
    Neil Kettle and Andy King
    IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems (TCAD), IEEE. (Note: Copyright held by IEEE 2007.)
    [ paper (pdf) - link - abstract ]
  • August 10-06
    - Proof of New Decompositional Results for Generalized Symmetries
    Neil Kettle and Andy King
    Technical Report 05-06, Computing Laboratory, University of Kent, Canterbury, Kent, CT2 7NF.
    [ paper (ps) - abstract ]
  • March 20-06
    - Widening ROBDDs with Prime Implicants
    Neil Kettle, Andy King, and Tadeusz Strzemecki
    In Holger Hermanns and Jens Palsberg, editors, 12th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), volume 3920 of Lecture Notes in Computer Science, pages 105-119. Springer-Verlag. (Note: see http://www.springer.de/comp/lncs/index.html.)
    [ paper (ps) - paper (pdf) - presentation (pdf) - link - abstract ]
  • February 16-06
    - Proof of New Implicational Relationships between Generalized Symmetries
    Neil Kettle and Andy King
    Technical Report 13-05, Computing Laboratory, University of Kent, Canterbury, Kent, CT2 7NF.
    [ paper (ps) - abstract ]
  • January 30-06
    - An Anytime Symmetry Detection Algorithm for ROBDDs
    Neil Kettle and Andy King
    In Hidetoshi Onodera, editor, 11th Asia and South Pacific Design Automation Conference (ASPDAC), pages 243-248. IEEE. (Note: Copyright held by IEEE 2006.)
    [ paper (ps) - paper (pdf) - presentation (pdf) - link - abstract ]

vuln.erabilities