Working with JSON-Formatted Data in Isabelle

JSON (JavaScript Object Notation) is common format for exchanging data. Thus, sometimes it would be handy to be able to “import” JSON-formatted data into Isabelle/HOL, e.g., as part of a datatype package (implemented in Isabelle/ML) for using the data as part of a system verification (in Isabelle/HOL).

Conformance Testing of Formal Semantics using Grammar-based Fuzzing

In our work “A Denotational Semantics of Solidity in Isabelle/HOL[1] we presented a formal semantics for Solidity, the most common language for implementing smart contracts. Such a formal semantics one of the corner stones of developing a formal verification approach that, mathematically, can prove the absence of certain types of bugs (e.g., such as the Parity Wallet bug that made USD 280mil worth of Ether inaccessible).

But, of course, any verification can only be as good as the underlying semantics. So, how do we ensure that our formal semantics actually captures the behavior of Solidity faithfully? This is the question we answer in our latest paper [2] that will be presented at the International Conference on Tests and Proofs.

The Link Between Digital Security and Privacy by Design and Skills Needs

Currently, the UK government pushes a concept called Digital Security by Design (DSbD) that focuses on utilizing novel hardware features to improve the security and trustworthiness of systems. Actually, Digital Security (and Privacy) by Design is a much broader concept focusing on security and privacy of systems right of systems right from the start of their development. And it also links to the - often misunderstood - concept of the Trusted Computing Base (TCB).