检索结果-内蒙古大学图书馆

Cerise: program Verification on a Capability Machine in the Presence of Untrusted Code

JOURNAL OF THE ACM 2024年第1期71卷 1-59页

作者： Georges, Aina Linn Gueneau, Armael Van Strydonck, Thomas Timany, Amin Trieu, Alix Devriese, Dominique Birkedal, Lars Max Planck Inst Software Syst Campus E1 5 D-66123 Saarbrucken Germany Univ Paris Saclay CNRS Lab Methodes Formelles ENS Paris SaclayInria Bat 650 Ada LovelaceRue Raimond Castaing F-91190 Gif Sur Yvette France Katholieke Univ Leuven Imec Distrinet Celestijnenlaan 200A Bus 2402 B-3001 Heverlee Belgium Aarhus Univ Abogade 34 DK-8200 Aarhus N Denmark ANSSI 51 Blvd Tour Maubourg F-75700 Paris 07 SP France

A capability machine is a type of CPU allowing fine-grained privilege separation using capabilities, machine words that represent certain kinds of authority. We present a mathematical model and accompanying proof methods that can be used for formal verification of functional correctness of programs running on a capability machine, even when they invoke and are invoked by unknown (and possibly malicious) code. We use a program logic called Cerise for reasoning about known code, and an associated logical relation, for reasoning about unknown code. The logical relation formally captures the capability safety guarantees provided by the capability machine. The Cerise program logic, logical relation, and all the examples considered in the paper have been mechanized using the Iris program logic framework in the Coq proof assistant. The methodology we present underlies recent work of the authors on formal reasoning about capability machines [Georges et al. 2021;Skorstengaard et al. 2019a;Van Strydonck et al. 2022], but was left somewhat implicit in those publications. In this paper we present a pedagogical introduction to the methodology, in a simpler setting (no exotic capabilities), and starting from minimal examples. We work our way up to new results about a heap-based calling convention and implementations of sophisticated object-capability patterns of the kind previously studied for high-level languages with object-capabilities, demonstrating that the methodology scales to such reasoning.

关键词： Capability machines capability safety universal contracts program logic separation logic CHERI

来源：评论

学校读者我要写书评

暂无评论

Partial correctness for probabilistic demonic programs

引用

THEORETICAL COMPUTER SCIENCE 2001年第1-2期266卷 513-541页

作者： McIver, AK Morgan, C Univ Oxford Comp Lab Programming Res Grp Oxford OX1 3QD England

Recent work in sequential program semantics has produced both an operational (He et al., Sci. Comput. programming 28(2, 3) (1997) 171-192) and an axiomatic (Morgan et al., ACM Trans. programming Languages Systems 18(3) (1996) 325-353;Seidel et al., Tech Report PRG-TR-6-96, programming Research group, February 1996) treatment of total correctness for probabilistic demonic programs, extending Kozen's original work (J. Comput. System Sci. 22 (1981) 328-350;Kozen, Proc. 15th ACM Symp. on Theory of Computing, ACM, New York, 1983) by adding demonic nondeterminism. For practical applications (e.g. combining loop invariants with termination constraints) it is important to retain the traditional distinction between partial and total correctness. Jones (Monograph ECS-LFCS-90-105, Ph.D. Thesis, Edinburgh University, Edinburgh, UK, 1990) defines probabilistic partial correctness for probabilistic, but again not demonic programs. In this paper we combine all the above, giving an operational and axiomatic framework for both partial and total correctness of probabilistic and demonic sequential programs;among other things, that provides the theory to support our earlier - and practical - publication on probabilistic demonic loops (Morgan, in: Jifeng et al. (Eds.), Proc. BCS-FACS Seventh Refinement Workshop, Workshops in Computing, Springer, Berlin, 1996). (C) 2001 Elsevier Science B.V. All rights reserved.

关键词： program logic verification probability partial correctness

来源：评论

学校读者我要写书评

暂无评论

A refinement calculus for the synthesis of verified hardware descriptions in VHDL

引用

ACM TRANSACTIONS ON programMING LANGUAGES AND SYSTEMS 1997年第4期19卷 586-616页

作者： Breuer, PT Kloos, CD Lopez, AM Madrid, NM Fernandez, LS UNIV POLITECN MADRID DEPT INGN SISTEMAS TELEMAT ETSI TELECOMUN E-28040 MADRID SPAIN

A formal refinement calculus targeted at system-level descriptions in the IEEE standard hardware description language VHDL is described here. Refinement can be used to develop hardware description code that is ''correct by construction.'' The calculus is closely related to a Hoare-style programming logic for VHDL and real-time systems in general. That logic and a semantics for a core subset of VHDL are described. The programming logic and the associated refinement calculus are shown to be complete. This means that if there is a code that can be shown to implement a. given specification, then it will be derivable from the specification via the calculus.

关键词： denotational semantics digital circuits formal verification program logic refinement timed logic VHDL

来源：评论

学校读者我要写书评

暂无评论

Generic weakest precondition semantics from monads enriched with order

引用

THEORETICAL COMPUTER SCIENCE 2015年 604卷 2-29页

作者： Hasuo, Ichiro Univ Tokyo Dept Comp Sci Tokyo 1138656 Japan

We devise a generic framework where a weakest precondition semantics, in the form of indexed posets, is derived from a monad whose Kleisli category is enriched by posets. It is inspired by Jacobs' recent identification of a categorical structure that is common in various predicate transformers, but adds generality in the following aspects: (1) different notions of modality (such as "may" vs. "must") are captured by Eilenberg-Moore algebras;(2) nested alternating branching like in games and in probabilistic systems with nondeterministic environments is modularly modeled by a monad on the Eilenberg-Moore category of another. (C) 2015 Elsevier B.V. All rights reserved.

关键词： program verification program logic Precondition calculus Nondeterminism Game Effect Algebra Coalgebra Categorical model Monad

来源：评论

学校读者我要写书评

暂无评论

MATCHING logic

引用

logicAL METHODS IN COMPUTER SCIENCE 2017年第4期13卷

作者： Rosu, Grigore Univ Illinois Urbana IL 61801 USA

This paper presents matching logic, a first-order logic (FOL) variant for specifying and reasoning about structure by means of patterns and pattern matching. Its sentences, the patterns, are constructed using variables, symbols, connectives and quantifiers, but no difference is made between function and predicate symbols. In models, a pattern evaluates into a power-set domain (the set of values that match it), in contrast to FOL where functions and predicates map into a regular domain. Matching logic uniformly generalizes several logical frameworks important for program analysis, such as: propositional logic, algebraic specification, FOL with equality, modal logic, and separation logic. Patterns can specify separation requirements at any level in any program configuration, not only in the heaps or stores, without any special logical constructs for that: the very nature of pattern matching is that if two structures are matched as part of a pattern, then they can only be spatially separated. Like FOL, matching logic can also be translated into pure predicate logic with equality, at the same time admitting its own sound and complete proof system. A practical aspect of matching logic is that FOL reasoning with equality remains sound, so off-the-shelf provers and SMT solvers can be used for matching logic reasoning. Matching logic is particularly well-suited for reasoning about programs in programming languages that have an operational semantics, but it is not limited to this.

关键词： program logic First-order logic Rewriting Verification

来源：评论

学校读者我要写书评

暂无评论

An Axiomatic Basis for Computer programming on the Relaxed Arm-A Architecture: The AxSL logic

引用

PROCEEDINGS OF THE ACM ON programMING LANGUAGES-PACMPL 2024年第POPL期8卷 604-637页

作者： Hammond, Angus Liu, Zongyuan Perami, Thibaut Sewell, Peter Birkedal, Lars Pichon-Pharabod, Jean Univ Cambridge Comp Lab JJ Thomson Ave Cambridge CB3 0FD England Aarhus Univ Abogade 34 DK-8200 Aarhus Denmark

Very relaxed concurrency memory models, like those of the Arm-A, RISC-V, and IBM Power hardware architectures, underpin much of computing but break a fundamental intuition about programs, namely that syntactic program order and the reads-from relation always both induce order in the execution. Instead, out-of-order execution is allowed except where prevented by certain pairwise dependencies, barriers, or other synchronisation. This means that there is no notion of the 'current' state of the program, making it challenging to design (and prove sound) syntax-directed, modular reasoning methods like Hoare logics, as usable resources cannot implicitly flow from one program point to the next. We present AxSL, a separation logic for the relaxed memory model of Arm-A, that captures the fine-grained reasoning underpinning the low-overhead synchronisation mechanisms used by high-performance systems code. In particular, AxSL allows transferring arbitrary resources using relaxed reads and writes when they induce inter-thread ordering. We mechanise AxSL in the Iris separation logic framework, illustrate it on key examples, and prove it sound with respect to the axiomatic memory model of Arm-A. Our approach is largely generic in the axiomatic model and in the instruction-set semantics, offering a potential way forward for compositional reasoning for other similar models, and for the combination of production concurrency models and full-scale ISAs.

关键词： relaxed memory models program logic separation logic Arm Iris

来源：评论

学校读者我要写书评

暂无评论

Summingbird: A Framework for Integrating Batch and Online MapReduce Computations

引用

PROCEEDINGS OF THE VLDB ENDOWMENT 2014年第13期7卷 1441-1451页

作者： Boykin, Oscar Ritchie, Sam O'Connell, Ian Lin, Jimmy Twitter Inc San Francisco CA 94103 USA

Summingbird is an open-source domain-specific language implemented in Scala and designed to integrate online and batch MapReduce computations in a single framework. Summingbird programs are written using dataflow abstractions such as sources, sinks, and stores, and can run on different execution platforms: Hadoop for batch processing (via Scalding/Cascading) and Storm for online processing. Different execution modes require different bindings for the dataflow abstractions (e.g., HDFS files or message queues for the source) but do not require any changes to the program logic. Furthermore, Summingbird can operate in a hybrid processing mode that transparently integrates batch and online results to efficiently generate up-to-date aggregations over long time spans. The language was designed to improve developer productivity and address pain points in building analytics solutions at Twitter where often, the same code needs to be written twice (once for batch processing and again for online processing) and indefinitely maintained in parallel. Our key insight is that certain algebraic structures provide the theoretical foundation for integrating batch and online processing in a seamless fashion. This means that Summingbird imposes constraints on the types of aggregations that can be performed, although in practice we have not found these constraints to be overly restrictive for a broad range of analytics tasks at Twitter.

关键词： Batch data processing Abstracting Problem oriented languages Social networking (online) Algebraic structures Domain specific languages Execution platforms Hybrid processing Message queues Online processing program logic Theoretical foundations

来源：评论

学校读者我要写书评

暂无评论

A Compositional Theory of Linearizability

引用

PROCEEDINGS OF THE ACM ON programMING LANGUAGES-PACMPL 2023年第POPL期7卷 1089-1120页

作者： Vale, Arthur Oliveira Shao, Zhong Chen, Yixuan Yale Univ New Haven CT 06520 USA

Compositionality is at the core of programming languages research and has become an important goal toward scalable verification of large systems. Despite that, there is no compositional account of linearizability, the gold standard of correctness for concurrent objects. In this paper, we develop a compositional semantics for linearizable concurrent objects. We start by showcasing a common issue, which is independent of linearizability, in the construction of compositional models of concurrent computation: interaction with the neutral element for composition can lead to emergent behaviors, a hindrance to compositionality. Category theory provides a solution for the issue in the form of the Karoubi envelope. Surprisingly, and this is the main discovery of our work, this abstract construction is deeply related to linearizability and leads to a novel formulation of it. Notably, this new formulation neither relies on atomicity nor directly upon happens-before ordering and is only possible because of compositionality, revealing that linearizability and compositionality are intrinsically related to each other. We use this new, and compositional, understanding of linearizability to revisit much of the theory of linearizability, providing novel, simple, algebraic proofs of the locality property and of an analogue of the equivalence with observational refinement. We show our techniques can be used in practice by connecting our semantics with a simple program logic that is nonetheless sound concerning this generalized linearizability.

关键词： linearizability game semantics concurrency program logic

来源：评论

学校读者我要写书评

暂无评论

Leveraging Rust Types for program Synthesis

引用

PROCEEDINGS OF THE ACM ON programMING LANGUAGES-PACMPL 2023年第PLDI期7卷 1414-1437页

作者： Fiala, Jonas Itzhaky, Shachar Muller, Peter Polikarpova, Nadia Sergey, Ilya Swiss Fed Inst Technol Dept Comp Sci Zurich Switzerland Technion Haifa Israel Univ Calif San Diego San Diego CA USA Natl Univ Singapore Singapore Singapore

The Rust type system guarantees memory safety and data-race freedom. However, to satisfy Rust's type rules, many familiar implementation patterns must be adapted substantially. These necessary adaptations complicate programming and might hinder language adoption. In this paper, we demonstrate that, in contrast to manual programming, automatic synthesis is not complicated by Rust's type system, but rather benefits in two major ways. First, a Rust synthesizer can get away with significantly simpler specifications. While in more traditional imperative languages, synthesizers often require lengthy annotations in a complex logic to describe the shape of data structures, aliasing, and potential side effects, in Rust, all this information can be inferred from the types, letting the user focus on specifying functional properties using a slight extension of Rust expressions. Second, the Rust type system reduces the search space for synthesis, which improves performance. In this work, we present the first approach to automatically synthesizing correct-by-construction programs in safe Rust. The key ingredient of our synthesis procedure is Synthetic Ownership logic, a new program logic for deriving programs that are guaranteed to satisfy both a user-provided functional specification and, importantly, Rust's intricate type system. We implement this logic in a new tool called RusSOL. Our evaluation shows the effectiveness of RusSOL, both in terms of annotation burden and performance, in synthesizing provably correct solutions to common problems faced by new Rust developers.

关键词： program synthesis program logic Rust type systems

来源：评论

学校读者我要写书评

暂无评论

Efficient and Provable Local Capability Revocation using Uninitialized Capabilities

引用

PROCEEDINGS OF THE ACM ON programMING LANGUAGES-PACMPL 2021年第POPL期5卷 1–30页

作者： Georges, Aina Linn Gueneau, Armael Van Strydonck, Thomas Timany, Amin Trieu, Alix Huyghebaert, Sander Devriese, Dominique Birkedal, Lars Aarhus Univ Aarhus Denmark Katholieke Univ Leuven Leuven Belgium Vrije Univ Brussel Brussels Belgium

Capability machines are a special form of CPUs that offer fine-grained privilege separation using a form of authority-carrying values known as capabilities. The CHERI capability machine offers local capabilities, which could be used as a cheap but restricted form of capability revocation. Unfortunately, local capability revocation is unrealistic in practice because large amounts of stack memory need to be cleared as a security precaution. In this paper, we address this shortcoming by introducing uninitialized capabilities: a new form of capabilities that represent read/write authority to a block of memory without exposing the memory's initial contents. We provide a mechanically verified program logic for reasoning about programs on a capability machine with the new feature and we formalize and prove capability safety in the form of a universal contract for untrusted code. We use uninitialized capabilities for making a previously-proposed secure calling convention efficient and prove its security using the program logic. Finally, we report on a proof-of-concept implementation of uninitialized capabilities on the CHERI capability machine.

关键词： capability machines local capabilities uninitialized capabilities capability safety universal contracts program logic capability revocation CHERI

来源：评论

学校读者我要写书评

暂无评论

建议与咨询留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

建议与咨询 留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案： 新增检索档案 确定 取消

请选择收藏分类： 新增自定义分类 确定 取消

通借通还

建议与咨询留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

请选择保存的检索档案：

请选择收藏分类：