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.
Several fully funded PhD scholarships for UK applicants are available in the
Security and Trust of Advanced Systems
Group
(Prof. Achim Brucker and Dr. Diego
Marmsoler) at the Department of Computer Science of the
University of Exeter, UK.
Smart contracts are programs, usually automating legal
agreements such as financial transactions. Thus, bugs in smart contracts
can lead to large financial losses. For example, an incorrectly initialized
contract was the root cause of the Parity Wallet bug that made USD
280mil worth of Ether inaccessible. Ether is the cryptocurrency of the
Ethereum blockchain that uses Solidity for expressing smart contracts.
The environmental impact of products is an important factor in buying decisions
of customers, and it is also an increasing concern of lawmakers. Hence, companies
are interested in determining the ecological footprint of their products.
Life-cycle assessment (LCA) is a standardized method for computing the
ecological footprint of a product.
