The focus of this proposal is on the detection and survival of wrong code compiler defects, which we argue present a cyber-security threat that has been largely ignored to date. First, incorrectly compiled code can introduce exploitable vulnerabilities that are not visible at the source code level, and thus cannot be detected by source-level static analysers. Second, incorrectly compiled code can undermine the reliability of the application, which can have dramatic repercussions in the context of safety-critical systems. Third, wrong code compiler defects can also be the target of some of the most insidious security attacks. A crafty attacker posing as an open source developer can introduce a compiler-bug-based backdoor into a security-critical application by adding a patch that looks perfectly innocent but which, when compiled with a certain compiler, yields binary code that allows the attacker to compromise the software. In this project, we aim to explore automated techniques that can detect and prevent such problems. In particular, we plan to investigate techniques for automatically finding compiler-induced vulnerabilities in real software, approaches for understanding the extent to which an attacker could maliciously modify an application to create a compiler-induced vulnerability, and methods for preventing against such vulnerabilities at runtime.

Software is woven into just about everything digital that we touch or depend upon: from communications, entertainment and consumer electronics - to railway, air-control, automotive, finance, defence, national infrastructure and health-care systems. The dependability of such software remains a major challenge. In 2002 it was estimated that software mistakes cost the US economy $59 Billion; more recent estimates have suggested an annual cost of more than $300 Billion worldwide. Dependability is therefore a key differentiator in commercial products. Whoever can cost-effectively crack the dependability challenge will have a major advantage. Conventional techniques used to ensure dependability are based around testing; and this can amount to half of the development time. Still, a fundamental problem of testing is that all combinations of inputs and conditions are not feasible. Formal approaches to software engineering use mathematics to ensure dependability. These have the advantage over conventional testing techniques that the software can be proven correct for all combinations of inputs and conditions. This is a result of using mathematics, and increases both the dependability and product quality. However, common bottlenecks of these approaches are limited availability of theorem proving skills and lack of automation provided by tools. Therefore they have often suffered from increased development time and costs when applied beyond niche markets such as safety and mission critical systems. Program verification is a formal software engineering technique where the source code is combined with a formal specification of desired behaviour. Mathematics is used to prove that the program satisfies its specification. Recently, there has been a wave of new program verifiers, where the underlying mathematics is hidden. Skills familiar to programmers are used to guide the proof in the program text rather than theorem proving skills; removing the "skill-barrier" associated with theorem provers and creating a more accessible discipline for a software engineer. Still, an open challenge is to reduce the amount of guidance that is required to complete the verification of a program - a challenge that has to be solved before program verification becomes a viable cost-effective mainstream software engineering discipline. This proposal addresses the automation challenge by enabling software engineers to encode patterns used to guide proofs directly in the program text as special programs. As a result, low-level and repetitive details, often resulting from a trial-and-error process, can be replaced by a higher-level underlying pattern. These can be re-used for similar tasks, liberating users from low-level and repetitive search tasks. As a pattern only needs to be developed once, less guidance will be needed - increasing automation and reducing development time and cost. The language used to write programs and guide proofs within a program verifier will be extended to enable software engineers to also encode their verification patterns. The extension should be as minimal as possible, to avoid reducing accessibility with new skill-barriers that have to be overcome. The development of such language requires a new understanding of how users guide program verifiers. We will focus on the Dafny program verifier; re-engineering the development process used in a selection of the available Dafny case studies; and developing and verifying new programs from scratch. In both cases, each step of the verification process will be captured, creating a catalogue of verification patterns. Based on this catalogue the language used within Dafny will be extended with a new special method called a `DTac' (Dafny Tactic). A verification pattern will be encoded as a DTac. Automation will be achieved by developing a new tool called Tacny that can read DTacs and apply them to other Dafny programs to automate the verification.

Abstracts are not currently available in GtR for all funded research. This is normally because the abstract was not required at the time of proposal submission, but may be because it included sensitive information such as personal details.

Tacit knowledge / 'knowing more than we can tell' / is knowledge that we know we have but can't articulate, or knowledge that we don't know that we have but nevertheless use. We rely on tacit knowledge to communicate effectively: we need not make every assumption we hold explicit, allowing us to focus on the essence of what we wish to communicate. As engineers concerned with the development of software and systems, however, we are taught to make our assumptions explicit, and indeed any kind of knowledge that is not made explicit makes our systems analysis more difficult and error prone. This problem is particularly acute during requirements engineering (RE) / when knowledge about the problem world and stakeholder requirements is elicited, and precise specifications of system structure and behaviour are developed. Requirements are often first communicated in natural language (NL), and are often ambiguous, incomplete, and inevitably full of undocumented assumptions and other omissions. Effective analysis of such requirements needs to surface this tacit knowledge / automatically or semi-automatically where possible / to document more precise requirements that can be relied upon by stakeholders to communicate effectively. Our proposed project aims to investigate techniques for analysing NL requirements, in order to discover, manage, and mitigate the negative effects of tacit knowledge in requirements. We propose to adopt an empirical approach to characterise and elicit tacit knowledge, and a constructive, theoretically-grounded but user-driven approach to develop practical techniques and tools to guide analysts concerned with the development of precise requirements for software-intensive systems.Our proposed approach is to mitigate the negative consequences of tacit knowledge by developing techniques to discover its differential impact on the understanding and use of requirements artefacts. This will enable the management of the effects of tacit knowledge, helping analysts identify where knowledge needs to be made explicit and providing tools capable of resolving at least some of the harmful effects. The results of our work will comprise tools and techniques for: improving the management of requirements information through automatic trace recovery; discovering the presence of tacit knowledge from the tracking of presuppositions and unprovenanced requirements; and the detection of nocuous ambiguity in requirements documents that imply potential for misinterpretation. A number of robust, lightweight natural language processing (NLP) techniques already exist that we will extend to develop our tools. If successful, the results of the work may have tangible benefits to RE practice. More fundamentally, by focusing on the down-stream symptoms of tacit knowledge, our work will make an important contribution to deepening our understanding of the role played by tacit knowledge in RE.

The use of computers and computer programs is pervasive nowadays, but every computer user knows that programs go wrong. While it is just annoying when our favourite text editor loses a bit of our work, the consequences are potentially much more serious when a computer program that, for instance, controls parts of an airplane goes wrong. Software validation and verification are central to the development of this sort of application. In fact, the software industry in general spends a very large amount of money in these activities. One of the measures taken to promote correctness of programs is the use of a restricted set of features available in programming languages. This usually means that most of the more recent advances in software engineering are left out. In this project, we propose to provide development, validation, and verification facilities that allow object-orientation and a modern real-time computational model to be used for the programming of safety-critical systems. In particular, we will work with one of the most popular programming languages: Java, or more specifically, its profiles for high-integrity engineering proposed by the Open Group. As our main case study, we will verify parts of the controller of the first Java Powered Industrial Robot, developed by Sun. One of our collaborators, a senior engineer in Sun tells in an interview that Distributed Real-Time Systems are really hard to build and the engineering community doesn't really know how to build them in a coherent repeatable way. (java.dzone.com/articles) Real-Time Java is entering the industrial automation and automotive markets. Lawyers did not allow the Java Robot to get anywhere near a human, even in a JavaOne conference demo. To proceed in that kind market, better support is needed.Programming is just one aspect of the development of a modern system; typically, a large number of extra artefacts are produced to guide and justify its design. Just like several models of a large building are produced before bricks and mortar are put together, several specification and design models of a program are developed and used before programs are written. These models assist in the validation and verification of the program. To take our civil engineering metaphor one step further, we observe that, just like there can be various models of a building that reflect several points of view, like electricity cabling, plumbing, and floor plans, for example, we also have several models of a system. Different modelling and design notations concentrate on different aspects of the program: data models, concurrent and reactive behaviour, timing, and so on. No single notation or technique covers all the aspects of the problem, and a combination of them needs to be employed in the development of large complex systems. In this project, we propose to investigate a novel integrated approach to validation and verification. Our aim is to provide a sound and practical technique that covers data modelling, concurrency, distribution, and timing. For that, we plan to investigate the extension and combined use of validation and verification techniques that have been successfully applied in industry. We do not seek an ad hoc combination of notations and tools, but a justified approach that provides a reliable foundation for the use of practical techniques. We will have succeeded if we verify a substantial part of the robot controller: using a model written in our notation, we will apply our techniques to verify parts of the existing implementation, execute it using our verified implementation of Safety-critical Java. Measure of success will be provided by our industrial partners and the influence of our results in their practice or business plans.