The CompCert C compiler provides the formal guarantee that the observable behaviour of the compiled code improves on the observable behaviour of the source code. In this paper, we present a formally verified C compile...
详细信息
The CompCert C compiler provides the formal guarantee that the observable behaviour of the compiled code improves on the observable behaviour of the source code. In this paper, we present a formally verified C compiler, CompCertS, which is essentially the CompCert compiler, albeit with a stronger formal guarantee: it gives a semantics to more programs and ensures that the memory consumption is preserved by the compiler. CompCertS is based on an enhanced memory model where, unlike CompCert but like Gcc, the binary representation of pointers can be manipulated much like integers and where, unlike CompCert, allocation may fail if no memory is available. The whole proof of CompCertS is a significant proof-effort and we highlight the crux of the novel proofs of 12 passes of the back-end and a challenging proof of an essential optimising pass of the front-end.
The CompCert C compiler provides the formal guarantee that the observable behaviour of the compiled code improves on the observable behaviour of the source code. In this paper, we present a formally verified C compile...
详细信息
ISBN:
(纸本)9783319661070
The CompCert C compiler provides the formal guarantee that the observable behaviour of the compiled code improves on the observable behaviour of the source code. In this paper, we present a formally verified C compiler, CompCertS, which is essentially the CompCert compiler, albeit with a stronger formal guarantee: it gives a semantics to more programs and ensures that the memory consumption is preserved by the compiler. CompCertS is based on an enhanced memory model where, unlike CompCert but like Gcc, the binary representation of pointers can be manipulated much like integers and where, unlike CompCert, allocation may fail if no memory is available. The whole proof of CompCertS is a significant proof-effort and we highlight the crux of the novel proofs of 12 passes of the back-end and a challenging proof of an essential optimising pass of the front-end.
Recent advances in hardware design have demonstrated mechanisms allowing a wide range of low-level security policies (or micro-policies) to be expressed using rules on metadata tags. We propose a methodology for defin...
详细信息
ISBN:
(纸本)9781467369497
Recent advances in hardware design have demonstrated mechanisms allowing a wide range of low-level security policies (or micro-policies) to be expressed using rules on metadata tags. We propose a methodology for defining and reasoning about such tag-based reference monitors in terms of a high-level "symbolic machine," and we use this methodology to define and formally verify micro-policies for dynamic sealing, compartmentalization, control-flow integrity, and memory safety;in addition, we show how to use the tagging mechanism to protect its own integrity. For each micro-policy, we prove by refinement that the symbolic machine instantiated with the policy's rules embodies a high-level specification characterizing a useful security property. Last, we show how the symbolic machine itself can be implemented in terms of a hardware rule cache and a software controller.
Process algebras like Timed CSP offer a convenient level of abstraction for the specification and verification of distributed embedded real-time systems. Complex systems can be specified in terms of interacting module...
详细信息
ISBN:
(纸本)9780769546094
Process algebras like Timed CSP offer a convenient level of abstraction for the specification and verification of distributed embedded real-time systems. Complex systems can be specified in terms of interacting modules whose interaction can be analyzed using the mechanisms of the process algebra. In this paper, we present a development approach that supports the construction of distributed real-time systems by exploiting Timed CSP's concept of modularity. Individual system components are refined to their low-level implementations and shown to be a formally correct implementation of their respective Timed CSP specifications. Their interaction can then be analyzed by composing the individual process specifications. The key idea underlying the presented approach is a formal relation between timed process algebraic specifications and implementations given in a general purpose programming language.
The formal verification of low-level code is a problem largely ignored by the academic community although it is seen as a major problem in industry. This paper examines the problems associated with verification at thi...
详细信息
The formal verification of low-level code is a problem largely ignored by the academic community although it is seen as a major problem in industry. This paper examines the problems associated with verification at this level and describes SPADE-8080, a verifiable sub-language of the Intel 8080. It also shows how programs written in SPADE-8080 can be analysed and formally verified with the SPADE software tools.
暂无评论