ORCID Profile
0000-0001-8883-0559
Current Organisation
Proofcraft
Does something not look right? The information on this page has been harvested from data sources that may not be up to date. We continue to work with information providers to improve coverage and quality. To report an issue, use the Feedback Form.
In Research Link Australia (RLA), "Research Topics" refer to ANZSRC FOR and SEO codes. These topics are either sourced from ANZSRC FOR and SEO codes listed in researchers' related grants or generated by a large language model (LLM) based on their publications.
Operating Systems | Computational Logic and Formal Languages | Computer Software |
Internet Hosting Services (incl. Application Hosting Services) | Application Tools and System Utilities
Publisher: ACM
Date: 18-09-2014
Publisher: Springer International Publishing
Date: 2014
Publisher: ACM
Date: 09-06-2014
Publisher: Springer Berlin Heidelberg
Date: 2010
Publisher: EasyChair
Date: 2017
DOI: 10.29007/C2F1
Abstract: The main security mechanism for enforcing memory isolation in operating systems is provided by page tables. The hardware-implemented Translation Lookaside Buffer (TLB) caches these, and therefore the TLB and its consistency with memory are security crit- ical for OS kernels, including formally verified kernels such as seL4. If performance is paramount, this consistency can be subtle to achieve yet, all major formally verified ker- nels currently leave the TLB as an assumption. In this paper, we present a formal model of the Memory Management Unit (MMU) for the ARM architecture which includes the TLB, its maintenance operations, and its derived properties. We integrate this specification into the Cambridge ARM model. We derive sufficient conditions for TLB consistency, and we abstract away the functional details of the MMU for simpler reasoning about executions in the presence of cached address translation, including complete and partial walks.
Publisher: Association for Computing Machinery (ACM)
Date: 07-2006
Abstract: We introduce Jinja, a Java-like programming language with a formal semantics designed to exhibit core features of the Java language architecture. Jinja is a compromise between the realism of the language and the tractability and clarity of its formal semantics. The following aspects are formalised: a big and a small step operational semantics for Jinja and a proof of their equivalence, a type system and a definite initialisation analysis, a type safety proof of the small step semantics, a virtual machine (JVM), its operational semantics and its type system, a type safety proof for the JVM a bytecode verifier, that is, a data flow analyser for the JVM, a correctness proof of the bytecode verifier with respect to the type system, and a compiler and a proof that it preserves semantics and well-typedness. The emphasis of this work is not on particular language features but on providing a unified model of the source language, the virtual machine, and the compiler. The whole development has been carried out in the theorem prover Isabelle/HOL.
Publisher: ACM
Date: 25-03-2016
Publisher: Springer International Publishing
Date: 2023
Publisher: Springer Science and Business Media LLC
Date: 20-02-2016
Publisher: IEEE
Date: 06-2012
Publisher: Institute of Electrical and Electronics Engineers (IEEE)
Date: 03-2012
DOI: 10.1109/MSP.2012.41
Publisher: IEEE
Date: 05-2015
DOI: 10.1109/ICSE.2015.85
Publisher: Springer Berlin Heidelberg
Publisher: Springer Berlin Heidelberg
Date: 2009
Publisher: Springer International Publishing
Date: 2015
Publisher: IEEE
Date: 06-2012
Publisher: Springer International Publishing
Date: 2014
Publisher: Springer Berlin Heidelberg
Date: 2010
Publisher: ACM
Date: 03-11-2013
Publisher: ACM
Date: 03-11-2014
Publisher: Association for Computing Machinery (ACM)
Date: 16-06-2013
Abstract: We extend the existing formal verification of the seL4 operating system microkernel from 9500 lines of C source code to the binary level. We handle all functions that were part of the previous verification. Like the original verification, we currently omit the assembly routines and volatile accesses used to control system hardware. More generally, we present an approach for proving refinement between the formal semantics of a program on the C source level and its formal semantics on the binary level, thus checking the validity of compilation, including some optimisations, and linking, and extending static properties proved of the source code to the executable. We make use of recent improvements in SMT solvers to almost fully automate this process. We handle binaries generated by unmodified gcc 4.5.1 at optimisation level 1, and can handle most of seL4 even at optimisation level 2.
Publisher: IEEE
Date: 05-2013
DOI: 10.1109/SP.2013.35
Publisher: Springer Berlin Heidelberg
Date: 2012
Publisher: Springer US
Date: 2010
Publisher: Springer Berlin Heidelberg
Date: 2008
Publisher: Elsevier BV
Date: 04-2003
Publisher: Association for Computing Machinery (ACM)
Date: 02-2014
DOI: 10.1145/2560537
Abstract: We present an in-depth coverage of the comprehensive machine-checked formal verification of seL4, a general-purpose operating system microkernel. We discuss the kernel design we used to make its verification tractable. We then describe the functional correctness proof of the kernel's C implementation and we cover further steps that transform this result into a comprehensive formal verification of the kernel: a formally verified IPC fastpath, a proof that the binary code of the kernel correctly implements the C semantics, a proof of correct access-control enforcement, a proof of information-flow noninterference, a sound worst-case execution time analysis of the binary, and an automatic initialiser for user-level systems that connects kernel-level access-control enforcement with reasoning about system behaviour. We summarise these results and show how they integrate to form a coherent overall analysis, backed by machine-checked, end-to-end theorems. The seL4 microkernel is currently not just the only general-purpose operating system kernel that is fully formally verified to this degree. It is also the only ex le of formal proof of this scale that is kept current as the requirements, design and implementation of the system evolve over almost a decade. We report on our experience in maintaining this evolving formally verified code base.
Publisher: Springer Science and Business Media LLC
Date: 17-03-2009
Publisher: Springer Science and Business Media LLC
Date: 02-2009
Publisher: ACM
Date: 28-10-2017
Publisher: Elsevier BV
Date: 2004
Publisher: Association for Computing Machinery (ACM)
Date: 06-2010
Publisher: Springer Berlin Heidelberg
Date: 2005
DOI: 10.1007/11591191_33
Publisher: Springer Berlin Heidelberg
Date: 2010
Publisher: Springer Berlin Heidelberg
Date: 2011
Publisher: Springer Berlin Heidelberg
Date: 2012
Publisher: Springer Berlin Heidelberg
Date: 2009
Publisher: ACM
Date: 31-08-2009
Publisher: ACM
Date: 04-10-2010
Publisher: Association for Computing Machinery (ACM)
Date: 04-09-2016
Abstract: We present a framework aimed at significantly reducing the cost of verifying certain classes of systems software, such as file systems. Our framework allows for equational reasoning about systems code written in our new language, Cogent. Cogent is a restricted, polymorphic, higher-order, and purely functional language with linear types and without the need for a trusted runtime or garbage collector. Linear types allow us to assign two semantics to the language: one imperative, suitable for efficient C code generation and one functional, suitable for equational reasoning and verification. As Cogent is a restricted language, it is designed to easily interoperate with existing C functions and to connect to existing C verification frameworks. Our framework is based on certifying compilation: For a well-typed Cogent program, our compiler produces C code, a high-level shallow embedding of its semantics in Isabelle/HOL, and a proof that the C code correctly refines this embedding. Thus one can reason about the full semantics of real-world systems code productively and equationally, while retaining the interoperability and leanness of C. The compiler certificate is a series of language-level proofs and per-program translation validation phases, combined into one coherent top-level theorem in Isabelle/HOL.
Publisher: Springer Berlin Heidelberg
Date: 2012
Publisher: Springer Berlin Heidelberg
Publisher: ACM
Date: 16-06-2013
Publisher: The Royal Society
Date: 04-09-2017
Abstract: We present recent work on building and scaling trustworthy systems with formal, machine-checkable proof from the ground up, including the operating system kernel, at the level of binary machine code. We first give a brief overview of the seL4 microkernel verification and how it can be used to build verified systems. We then show two complementary techniques for scaling these methods to larger systems: proof engineering, to estimate verification effort and code roof co-generation, for scalable development of provably trustworthy applications. This article is part of the themed issue ‘Verified trustworthy software systems’.
Publisher: Association for Computing Machinery (ACM)
Date: 07-2007
Abstract: As computer systems become increasingly mission-critical, used in life-critical situations, and relied upon to protect intellectual property, operating-system reliability is becoming an ever growing concern. In the past, mission- and life-critical embedded systems consisted of simple microcontrollers running a small amount of software that could be validated using traditional and informal techniques. However, with the growth of software complexity, traditional techniques for ensuring software reliability have not been able to keep up, leading to an overall degradation of reliability. This paper argues that microkernels are the best approach for delivering truly trustworthy computer systems in the foreseeable future. It presents the NICTA operating-systems research vision, centred around the L4 microkernel and based on four core projects. The seL4 project is designing an improved API for a secure microkernel, L4, verified will produce a full formal verification of the microkernel, Potoroo combines execution-time measurements with static analysis to determine the worst case execution profiles of the kernel, and CAmkES provides a component architecture for building systems that use the microkernel. Through close collaboration with Open Kernel Labs (a NICTA spinoff) the research output of these projects will make its way into products over the next few years.
Publisher: Springer Science and Business Media LLC
Date: 2003
Publisher: ACM
Date: 11-10-2009
Publisher: ACM
Date: 30-08-2010
Publisher: ACM
Date: 17-01-2007
Publisher: IEEE
Date: 05-2013
Publisher: Springer Berlin Heidelberg
Date: 2013
Publisher: Springer Berlin Heidelberg
Date: 2012
Publisher: Springer International Publishing
Date: 2016
Publisher: Walter de Gruyter GmbH
Date: 02-2005
DOI: 10.1524/ITIT.47.2.107.62257
Abstract: Der Bytecode Verifier ist ein essenzieller Bestandteil der Sicherheitsarchitektur der Programmierplattform Java. Die vorliegende Dissertation stellt eine formale, ausführbare Spezifikation des Bytecode Verifiers vor sowie den Beweis, dass diese korrekt ist. Die Formalisierung, vollständig im Theorembeweiser Isabelle durchgeführt, besteht aus einem abstrakten Framework für Bytecode-Verifikation, das mit zunehmend ausdrucksstarken Typsystemen instanziiert wird. Diese decken sämtliche wichtigen Eigenschaften der Java-Plattform ab. Die Formalisierung liefert zwei ausführbare, verifizierte Bytecode Verifier: den Standard-Algorithmus, wie er auf normalen Desktop-Rechnern benutzt wird, und einen Lightweight Bytecode Verifier für eingebettete Systeme mit Ressourcenbeschränkungen wie z.B. Java SmartCards.
Publisher: Association for Computing Machinery (ACM)
Date: 11-2014
DOI: 10.1007/S00165-014-0296-9
Abstract: It is a great verification challenge to prove properties of complete computer systems on the source code level. The L4.verified project achieved a major step towards this goal by mechanising a proof of functional correctness of the seL4 kernel. They expressed correctness in terms of data refinement with a coarse-grained specification of the kernel’s execution environment. In this paper, we strengthen the original correctness theorem in two ways. First, we convert the previous abstraction relations into projection functions from concrete to abstract states. Second, we revisit the specification of the kernel’s execution environment: we introduce the notion of virtual memory based on the kernel data structures, we distinguish in idual user programs that run on top of the kernel and we restrict the memory access of each of these programs to its virtual memory. Through our work, properties like the separation of user programs gain meaning. This paves the way for proving security properties like non-interference of user programs. Furthermore, our extension of L4.verified’s proof facilitates the verification of properties about complete software systems based on the seL4 kernel. Besides the seL4-specific results, we report on our work from an engineering perspective to exemplify general challenges that similar projects are likely to encounter. Moreover, we point out the advantages of using projection functions in L4.verified’s verification approach and for stepwise refinement in general.
Publisher: Elsevier BV
Date: 04-2015
Publisher: ACM
Date: 04-09-2016
Publisher: Wiley
Date: 11-2001
DOI: 10.1002/CPE.597
Start Date: 2019
End Date: 06-2023
Amount: $660,000.00
Funder: Australian Research Council
View Funded Activity