Computing Reviews
Today's Issue Hot Topics Search Browse Recommended My Account Log In
Review Help
Search
An automatic proving approach to parameterized verification
Li Y., Duan K., Jansen D., Pang J., Zhang L., Lv Y., Cai S. ACM Transactions on Computational Logic19 (4):1-25,2018.Type:Article
Date Reviewed: Feb 20 2019

Network and security protocols occasionally require important but difficult to authenticate parameters such as the number in a communication party. The existing formal proofs of algorithms for verifying the required parameters in protocols by humans are cumbersome. How should a reliable system be designed for the automatic validation of the various parameters in cache coherence, security, network, wireless, and other open systems interconnection layers protocols? Li et al. present a generic method for validating the parameters in protocols that facilitate interoperability and communications by users with different devices and software. The approach initially determines the supplementary invariables, their dependence graph associations and rules from inconsequential occurrences of a protocol, prior to automatically generalizing and sending the parameters to a theorem authenticator called Isabelle.

The authors succinctly review the inadequacies of previous studies on the verification of protocol parameters. Certainly, ascertaining the correctness of protocol parameters requires formal proofs, beyond parameter abstraction and partial computation of the accessible set of indistinguishable invariants. A theorem prover ought to use precise predicate logic for routinely verifying properties that are derived from the subsidiary invariants of protocol parameters.

To what extent do parametric protocols satisfy the stated functional requirements? The paper presents paraVerifier, a tool for discovering the satisfiability of protocol requirements. The tool contains components that accept protocol rules and requirements, as well as automatically locate alternative add-on invariants, label their proof interconnections, and convert them into proof scripts for attesting requirements. The archetype paraVerifier is successfully applied to automatically verify the parameters of protocols in applications such as FLASH, archetypal snoopy bus, and directory-based cache coherence benchmarks.

The significant contributions of this research include the distinction between different types of proof dependencies for providing alternative induction strategies for a theorem prover; the automatic recognition of important pairs of invariants and guarded commands based on associations among parameters and satisfiability of conditional expressions in transition states; the application of an abstract and a precise model to speed up the validation of candidate invariants in protocols with large models; and the use of a model to verify the relevance of candidate invariants in small actual occurrences.

The safety and liveness properties of different intercommunication network protocols are crucial for monitoring activities in our new Internet of Things (IoT) world. I call on artificial intelligence experts, network designers, and administrators to read and render opinions on the paper’s mathematical ideas for the automatic validation of protocol parameters and their broader application domains.

Reviewer:  Amos Olagunju Review #: CR146440 (1905-0169)
Bookmark and Share
  Reviewer Selected
Featured Reviewer
 
 
Security and Protection (C.2.0 ... )
 
 
Network Protocols (C.2.2 )
 
Would you recommend this review?
yes
no
Other reviews under "Security and Protection": Date
Introduction to data security and controls (2nd ed.)
Edward R. I., QED Information Sciences, Inc., Wellesley, MA, 1991. Type: Book (9780894353864)
Aug 1 1992
Security for computer networks: an introduction to data security in teleprocessing and electronic funds transfer
Davies D., Price W., John Wiley & Sons, Inc., New York, NY, 1984. Type: Book (9780471900634)
Oct 1 1985
The development and proof of a formal specification for a multilevel secure system
Glasgow J., Macewen G. ACM Transactions on Computer Systems 5(2): 151-184, 1987. Type: Article
Oct 1 1987
more...

E-Mail This Printer-Friendly
Send Your Comments
Contact Us
Reproduction in whole or in part without permission is prohibited.   Copyright 1999-2024 ThinkLoud®
Terms of Use
| Privacy Policy