blob: 21a512510b7feae318230b97aacb532a4084e5cd (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
|
#+options: ':t *:t -:t ::t <:t H:3 \n:nil ^:t arch:headline author:t
#+options: broken-links:nil c:nil creator:nil d:(not "LOGBOOK") date:t e:t
#+options: email:nil f:t inline:t num:t p:nil pri:nil prop:nil stat:t tags:t
#+options: tasks:t tex:t timestamp:t title:t toc:t todo:t |:t
#+title: Semantics of an embedded vector architecture for formal verification of software
#+date: \today
#+author: Greg Brown
#+email: greg.brown@cl.cam.ac.uk
#+language: en-GB
#+select_tags: export
#+exclude_tags: noexport
#+creator: Emacs 27.2 (Org mode 9.6)
#+cite_export: biblatex
#+bibliography: ./thesis.bib
#+latex_class: article
#+latex_class_options: [twocolumn,a4paper]
#+latex_header: \usepackage[hyperref=true,url=true,backend=biber,natbib=true]{biblatex}
#+latex_header: \usepackage{savetrees}
#+latex_compiler: pdflatex
#+begin_abstract
All good implementations of any algorithm should be correct and fast. To
maximise performance some algorithms are written in hand-tuned assembly. This
can introduce subtle bugs that invalidate correctness or other safety
properties. Whilst tools exists to help formally verify these algorithms, none
are designed to target the recent M-profile Vector Extension for the Armv8.1-M
architecture. This work describes a denotational and Hoare logic semantics for
the language used to specify the instructions, and attempts to use them to
formally verify the correctness of hand-written assembly for cryptographic
applications.
#+end_abstract
* Introduction
* Arm Pseudocode
* Denotational Semantics
* Hoare Semantics
* Mathematical Proofs
* Conclusions
#+print_bibliography:
|
