Scott Constable

A Formally Verified Heap Allocator

2018 · Syracuse University Libraries (Syracuse University)

We present the formal verification of a heap allocator written in C. We use the Isabelle/HOL proof assistant to formally verify the correctness of the heap allocator at the source code level. The C source …

STATIC ENFORCEMENT OF TERMINATION-SENSITIVE NONINTERFERENCE USING THE C++ TEMPLATE TYPE SYSTEM

2018 · Syracuse University Libraries (Syracuse University)

A side channel is an observable attribute of program execution other than explicit communication, e.g., power usage, execution time, or page fault patterns. A side-channel attack occurs when a malicious adversary observes program secrets through …