Jonathan P. Bowen

Jonathan P. Bowen, Henri Habrias

Jean-Raymond Abrial is one of the central figures in the development of formal methods for software and systems engineering. Over a career spanning more than five decades, he has played a decisive role in the creation of the Z specification notation, the B-Method, and Event-B, and in demonstrating their applicability to large-scale industrial systems. This paper presents a scholarly biographical account of Abrial's life and work, tracing the evolution of his ideas from early work on real-time languages and databases, through foundational contributions to formal specification, refinement, and proof, to the development of industrial-strength tool support such as the Atelier~B and the Rodin platform. The paper situates Abrial's contributions within their historical, intellectual, and industrial contexts, and assesses their lasting impact on software engineering and formal reasoning about programs.

Peter T. Breuer, Jonathan P. Bowen

This paper first describes an `obfuscating' compiler technology developed for encrypted computing, then examines if the trivial case without encryption produces much-sought indistinguishability obfuscation.

Jonathan P. Bowen

The original European ESPRIT ProCoS I and II projects on Provably Correct Systems} took place around a quarter of a century ago. Since then the legacy of the initiative has spawned many researchers with careers in formal methods. One of the leaders on the ProCoS projects was Ernst-Rüdiger Olderog. This paper charts the influence of the ProCoS projects and the subsequent ProCoS-WG Working Group, using Prof. Dr Olderog as an example. The community of researchers surrounding an initiative such as ProCoS is considered in the context of the social science concept of a Community of Practice (CoP) and the collaborations undertaken through coauthorship of and citations to publications. Consideration of citation metrics is also included.

Peter T. Breuer, Jonathan P. Bowen

Since fully homomorphic encryption and homomorphically encrypted computing preserve algebraic identities such as 2*2=2+2, a natural question is whether this extremely utilitarian feature also sets up cryptographic attacks that use the encrypted arithmetic operators to generate or identify the encryptions of known constants. In particular, software or hardware might use encrypted addition and multiplication to do encrypted division and deliver the encryption of x/x=1. That can then be used to generate 1+1=2, etc, until a complete codebook is obtained. This paper shows that there is no formula or computation using 32-bit multiplication x*y and three-input addition x+y+z that yields a known constant from unknown inputs. We characterise what operations are similarly `safe' alone or in company, and show that 32-bit division is not safe in this sense, but there are trivial modifications that make it so.

Peter T. Breuer, Jonathan P. Bowen

We ask whether two or more images of arithmetic may inhabit the same space via different encodings. The answers have significance for a class of processor design that does all its computation in an encrypted form, without ever performing any decryption or encryption itself. Against the possibility of algebraic attacks against the arithmetic in a `crypto-processor' (KPU) we propose a defence called `ABC encryption' and show how this kind of encryption makes it impossible for observations of the arithmetic to be used by an attacker to discover the actual values. We also show how to construct such encrypted arithmetics.

Peter T. Breuer, Jonathan P. Bowen

Sometimes machine code turns out to be a better target for verification than source code. RISC machine code is especially advantaged with respect to source code in this regard because it has only two instructions that access memory. That architecture forms the basis here for an inference system that can prove machine code safe against `hardware aliasing', an effect that occurs in embedded systems. There are programming memes that ensure code is safe from hardware aliasing, but we want to certify that a given machine code is provably safe.

Stefania Boiano, Jonathan P. Bowen, Giuliano Gaia

The paper discusses the experience of producing and distributing an iPhone app for promotion of the Maltese Cultural Heritage on behalf of the Malta Tourism Authority. Thanks to its position at the heart of the Mediterranean Sea, Malta has been a crossroads of civilisations whose traces are still visible today, leaving a particularly rich and varied cultural heritage, from megalithic temples to baroque palaces and Caravaggio masterpieces. Conveying all these different aspects within a single application, using textual, visual, and audio means, has raised many different issues about the planning and production of cultural content for mobile usage, together with usability aspects regarding design and distribution of a mobile app. In this paper, we outline all of these aspects, focusing on the design and planning strategies for a long-term user commitment and how to evaluate results for cultural mobile applications. We include experience of all the steps of developing a mobile app, information that is of possible benefit to other app developers in the cultural sector.