X-by-C: Non-functional security challenges

Abstract

Correctness-by-Construction (C-by-C) approaches software development as formal engineering and builds correct code by iterating from a correct specification. However, C-by-C is focused on functional properties of the system. X-by-Construction (X-by-C) extends C-by-C to also consider non-function properties concerning aspects such as security, dependability, reliability or energy consumption. In this work we consider the challenges of applying X-by-C to non-functional security properties such as side-channel attacks. We demonstrate how such non-functional security can be captured and reasoned about in an X-by-C manner, yielding the benefit of C-by-C for non-functional properties and security challenges.