High Confidence Software and Systems Conference 2016

file

Visible to the public Combinatorial Coverage Analysis of Subsets of the TLS Cipher Suite Registry

ABSTRACT
We present a combinatorial coverage measurement for (subsets) of the TLS cipher suite registries by analyzing the specific ciphers of IANA, ENISA, BSI, Mozilla and NSA Suite B. Our findings contribute towards the design of quality measures of recommended ciphers for TLS and also lead to important questions regarding the future development of TLS.

file

Visible to the public Measuring Protocol Strength with Security Goals

ABSTRACT
Flaws in published standards for security protocols are found regularly, often after systems implementing those standards have been deployed. Because of deployment constraints and disagreements among stakeholders, different fixes may be proposed and debated. In this process, security improvements must be balanced with issues of functionality and compatibility.

file

Visible to the public Formal Verification of C Programs with Floating-Point Computations: Certified Error Bounds for Signal Processing

ABSTRACT
In this technical talk, I will present our results related to the certification of floating-point error bounds in C implementations of signal processing algorithms. In particular, this relates to the topic of reasoning about the uncertainty caused by the noise arising from floating-point rounding errors and approximate computations in C programs.

file

Visible to the public Programming Uncertain <T>hings

ABSTRACT
Innovation flourishes with good abstractions. For instance, codification of the IEEE Floating Point standard in 1985 was critical to the subsequent success of scientific computing. Programming languages currently lack appropriate abstractions for uncertain data. Applications already use estimates from sensors, machine learning, big data, humans, and approximate algorithms, but most programming languages do not help developers address correctness, programmability, and optimization problems due to estimates.

file

Visible to the public Safety-Constrained Reinforcement Learning for MDPs

ABSTRACT
Many formal system models are inherently stochastic, consider for instance randomized distributed algorithms (where randomization breaks the symmetry between processes), security (e.g., key generation at encryption), systems biology (where species randomly react depending on their concentration), or embedded systems (interacting with unknown and varying environments).