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).

Ever wondered how to verify smart contracts written in Solidy? Thanks to our deep embedding of Solidty into Isabelle/HOL, you can now start verifying smart contracts in Isabelle.

We are proud to announce the release of Isabelle/DOF 1.3.0. Isabelle/DOF is a Document Ontology Framework on top of Isabelle 2021-1. Isabelle/DOF allows for both conventional typesetting and formal development.

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.

A large part of an academic’s life is writing grant proposals that are submitted to funding agencies. One of the UK’s funding agencies that supports research in security, safety, and correctness of systems is EPSRC. EPSRC officially requires proposal to follow a certain layout, that is summarized on the EPSRC website as follows:

We are proud to announce the release of Isabelle/DOF 1.2.0. Isabelle/DOF is a novel Document Ontology Framework on top of Isabelle. Isabelle/DOF allows for both conventional typesetting and formal development.

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).

As part of the launch of the UK’s new Cyber Security Strategy it has been announced that we are participants of a successful demonstrator project. The project is led by Beam Connectivity.