An official website of the United States government
Proving the correctness of a distributed protocol is a challenging endeavor. Central to this task is finding an inductive invariant for the protocol. Currently, automated invariant inference algorithms require developers to describe protocols using a restricted logic. If the developer wants to prove a protocol expressed without these restrictions, they must devise an inductive invariant manually. We propose an approach that simplifies and partially automates finding the inductive invariant of a distributed protocol, as well as proving that it really is an invariant. The key insight is to identify an invariant taxonomy that divides invariants into Regular Invariants, which have one of a few simple low-level structures, and Protocol Invariants, which capture the higher-level host relationships that make the protocol work. Building on the insight of this taxonomy, we describe the Kondo methodology for proving the correctness of a distributed protocol modeled as a state machine. The developer first manually devises the Protocol Invariants by proving a synchronous version of the protocol correct. In this simpler version, sends and receives are replaced with atomic variable assignments. The Kondo tool then automatically generates the asynchronous protocol description, Regular Invariants, and proofs that the Regular Invariants are inductive on their own. Finally, Kondo combines these with the synchronous proof into a draft proof of the asynchronous protocol, which may then require a small amount of user effort to complete. Our evaluation shows that Kondo reduces developer effort for a wide variety of distributed protocols.
more »
« less
Growing freshwater sponges from gemmules in the laboratory v1
This is a basic protocol for growing freshwater sponges from gemmules in the laboratory. We specifically developed this protocol for working with Ephydatia muelleri, but have used it for other species as well. This protocol is good for cleaning gemmules, and removing contaminating protists, fungi, and bacteria.
more »
« less
- Award ID(s):
- 2015608
- PAR ID:
- 10561028
- Publisher / Repository:
- Protocols.io
- Date Published:
- Format(s):
- Medium: X
- Sponsoring Org:
- National Science Foundation
More Like this
-
-
Standardized protocols for absolute quantification of potato virus Y (PVY) from potato tissue is critical for host-virus dynamic studies. Here, we developed a standardized protocol using a cloned viral sequence as standards to detect and quantify PVY. Starting with total RNA, concentrated via column-based kit, this protocol is able to detect approximately 50 viral copies/reaction from multiple PVY strains. Validation of this protocol confirmed linearity across 8 orders of magnitude with high repeatability, reproducibility and statistical robustness across three independent runs. This protocol offers reliable PVY quantification to manage potato crop health and enables comparative studies with other viral systems.more » « less
-
Mestre, Julián; Wirth, Anthony (Ed.)In his 2018 paper, Herlihy introduced an atomic protocol for multi-party asset swaps across different blockchains. Practical implementation of this protocol is hampered by its intricacy and computational complexity, as it relies on elaborate smart contracts for asset transfers, and specifying the protocol’s steps on a given digraph requires solving an NP-hard problem of computing longest paths. Herlihy left open the question whether there is a simple and efficient protocol for cross-chain asset swaps in arbitrary digraphs. Addressing this, we study HTLC-based protocols, in which all asset transfers are implemented with standard hashed time-lock smart contracts (HTLCs). Our main contribution is a full characterization of swap digraphs that have such protocols, in terms of so-called reuniclus graphs. We give an atomic HTLC-based protocol for reuniclus graphs. Our protocol is simple and efficient. We then prove that non-reuniclus graphs do not have atomic HTLC-based swap protocols.more » « less
-
Abstract Protein activity is generally functionally integrated and spatially restricted to key locations within the cell. Knocksideways experiments allow researchers to rapidly move proteins to alternate or ectopic regions of the cell and assess the resultant cellular response. Briefly, individual proteins to be tested using this approach must be modified with moieties that dimerize under treatment with rapamycin to promote the experimental spatial relocalizations. CRISPR technology enables researchers to engineer modified protein directly in cells while preserving proper protein levels because the engineered protein will be expressed from endogenous promoters. Here we provide straightforward instructions to engineer tagged, rapamycin‐relocalizable proteins in cells. The protocol is described in the context of our work with the microtubule depolymerizer MCAK/Kif2C, but it is easily adaptable to other genes and alternate tags such as degrons, optogenetic constructs, and other experimentally useful modifications. Off‐target effects are minimized by testing for the most efficient target site using a split‐GFP construct. This protocol involves no proprietary kits, only plasmids available from repositories (such as addgene.org). Validation, relocalization, and some example novel discoveries obtained working with endogenous protein levels are described. A graduate student with access to a fluorescence microscope should be able to prepare engineered cells with spatially controllable endogenous protein using this protocol. © 2023 The Authors. Current Protocols published by Wiley Periodicals LLC. Basic Protocol 1: Choosing a target site for gene modification Basic Protocol 2: Design of gRNA(s) for targeted gene modification Basic Protocol 3: Split‐GFP test for target efficiency Basic Protocol 4: Design of the recombination template and analytical primers Support Protocol 1: Design of primers for analytical PCR Basic Protocol 5: Transfection, isolation, and validation of engineered cells Support Protocol 2: Stable transfection of engineered cells with binding partnersmore » « less
-
Automated Attack Synthesis by Extracting Finite State Machines from Protocol Specification DocumentsHols, Thorsten Holz; Ristenpart, Thomas (Ed.)Automated attack discovery techniques, such as attacker synthesis or model-based fuzzing, provide powerful ways to ensure network protocols operate correctly and securely. Such techniques, in general, require a formal representation of the protocol, often in the form of a finite state machine (FSM). Unfortunately, many protocols are only described in English prose, and implementing even a simple network protocol as an FSM is time-consuming and prone to subtle logical errors. Automatically extracting protocol FSMs from documentation can significantly contribute to increased use of these techniques and result in more robust and secure protocol implementations.In this work we focus on attacker synthesis as a representative technique for protocol security, and on RFCs as a representative format for protocol prose description. Unlike other works that rely on rule-based approaches or use off-the-shelf NLP tools directly, we suggest a data-driven approach for extracting FSMs from RFC documents. Specifically, we use a hybrid approach consisting of three key steps: (1) large-scale word-representation learning for technical language, (2) focused zero-shot learning for mapping protocol text to a protocol-independent information language, and (3) rule-based mapping from protocol-independent information to a specific protocol FSM. We show the generalizability of our FSM extraction by using the RFCs for six different protocols: BGPv4, DCCP, LTP, PPTP, SCTP and TCP. We demonstrate how automated extraction of an FSM from an RFC can be applied to the synthesis of attacks, with TCP and DCCP as case-studies. Our approach shows that it is possible to automate attacker synthesis against protocols by using textual specifications such as RFCs.more » « less
- Free Publicly Accessible Full Text
-
Accepted Manuscript1.0
- Posted Content:
- https://doi.org/10.17504/protocols.io.x54v9dkj4g3e/v1
