Data

Tools

Indexes

Applications

Experiments

Open Source Science

reusableprotocolverificationlibrary

https://github.com/viperproject/reusableprotocolverificationlibrary

Science Score: 75.0%

This score indicates how likely this project is to be science-related based on various indicators:

  • ✓
    CITATION.cff file
    Found CITATION.cff file
  • ✓
    codemeta.json file
    Found codemeta.json file
  • ✓
    .zenodo.json file
    Found .zenodo.json file
  • ✓
    DOI references
    Found 8 DOI reference(s) in README
  • ✓
    Academic publication links
    Links to: arxiv.org
  • ○
    Academic email domains
  • ✓
    Institutional organization owner
    Organization viperproject has institutional domain (viper.ethz.ch)
  • ○
    JOSS paper metadata
  • ○
    Scientific vocabulary similarity
    Low similarity (10.3%) to scientific vocabulary
Last synced: 7 months ago · JSON representation ·

Repository

Basic Info
  • Host: GitHub
  • Owner: viperproject
  • Language: Go
  • Default Branch: main
  • Size: 369 KB
Statistics
  • Stars: 3
  • Watchers: 10
  • Forks: 0
  • Open Issues: 0
  • Releases: 0
Created over 2 years ago · Last pushed 7 months ago
Metadata Files
Readme Citation

README.md

A Generic Methodology for the Modular Verification of Security Protocol Implementations -- Reusable Verification Library

Reusable Verification Library

This repository hosts the Reusable Verification Library as a Go module, which enables easy integration into Go projects. This module simplifies verifying security properties for protocol implementations as described in the paper "A Generic Methodology for the Modular Verification of Security Protocol Implementations", published at ACM CCS '23 [published version] [extended version]. The entire artifact for this paper, which includes this verfication library, is available here and has been archived on Zenodo (DOI: 10.5281/zenodo.8330913). The paper can be cited as follows (for BibTeX): BibTex @InProceedings{ArquintSchwerhoffMehtaMueller23, author = {Arquint, Linard and Schwerhoff, Malte and Mehta, Vaibhav and M\"uller, Peter}, title = {A Generic Methodology for the Modular Verification of Security Protocol Implementations}, year = {2023}, isbn = {9798400700507}, publisher = {Association for Computing Machinery}, address = {New York, NY, USA}, booktitle = {Proceedings of the 2023 ACM SIGSAC Conference on Computer and Communications Security}, pages = {1377-1391}, numpages = {15}, keywords = {protocol implementation verification, symbolic security, separation logic, automated verification, injective agreement, forward secrecy}, location = {Copenhagen, Denmark}, series = {CCS '23}, doi = {10.1145/3576915.3623105}, url = {https://doi.org/10.1145/3576915.3623105}, urltext = {Publisher}, url1 = {https://pm.inf.ethz.ch/publications/ArquintSchwerhoffMehtaMueller23.pdf}, url1text = {PDF}, abstract = {Security protocols are essential building blocks of modern IT systems. Subtle flaws in their design or implementation may compromise the security of entire systems. It is, thus, important to prove the absence of such flaws through formal verification. Much existing work focuses on the verification of protocol *models*, which is not sufficient to show that their *implementations* are actually secure. Verification techniques for protocol implementations (e.g., via code generation or model extraction) typically impose severe restrictions on the used programming language and code design, which may lead to sub-optimal implementations. In this paper, we present a methodology for the modular verification of strong security properties directly on the level of the protocol implementations. Our methodology leverages state-of-the-art verification logics and tools to support a wide range of implementations and programming languages. We demonstrate its effectiveness by verifying memory safety and security of Go implementations of the Needham-Schroeder-Lowe, Diffie-Hellman key exchange, and WireGuard protocols, including forward secrecy and injective agreement for WireGuard. We also show that our methodology is agnostic to a particular language or program verifier with a prototype implementation for C.} }

Maintainer: Linard Arquint

Owner

  • Name: Viper Project
  • Login: viperproject
  • Kind: organization
  • Location: ETH Zurich

Verification Infrastructure for Permission-​based Reasoning

Citation (CITATION.bib) 

@InProceedings{ArquintSchwerhoffMehtaMueller23,
  author = {Arquint, Linard and Schwerhoff, Malte and Mehta, Vaibhav and M\"uller, Peter},
  title = {A Generic Methodology for the Modular Verification of Security Protocol Implementations},
  year = {2023},
  isbn = {9798400700507},
  publisher = {Association for Computing Machinery},
  address = {New York, NY, USA},
  booktitle = {Proceedings of the 2023 ACM SIGSAC Conference on Computer and Communications Security},
  pages = {1377-1391},
  numpages = {15},
  keywords = {protocol implementation verification, symbolic security, separation logic, automated verification, injective agreement, forward secrecy},
  location = {Copenhagen, Denmark},
  series = {CCS '23},
  doi = {10.1145/3576915.3623105},
  url = {https://doi.org/10.1145/3576915.3623105},
  urltext = {Publisher},
  url1 = {https://pm.inf.ethz.ch/publications/ArquintSchwerhoffMehtaMueller23.pdf},
  url1text = {PDF},
  abstract = {Security protocols are essential building blocks of modern IT systems. Subtle flaws in their design or implementation may compromise the security of entire systems. It is, thus, important to prove the absence of such flaws through formal verification. Much existing work focuses on the verification of protocol *models*, which is not sufficient to show that their *implementations* are actually secure. Verification techniques for protocol implementations (e.g., via code generation or model extraction) typically impose severe restrictions on the used programming language and code design, which may lead to sub-optimal implementations. In this paper, we present a methodology for the modular verification of strong security properties directly on the level of the protocol implementations. Our methodology leverages state-of-the-art verification logics and tools to support a wide range of implementations and programming languages. We demonstrate its effectiveness by verifying memory safety and security of Go implementations of the Needham-Schroeder-Lowe, Diffie-Hellman key exchange, and WireGuard protocols, including forward secrecy and injective agreement for WireGuard. We also show that our methodology is agnostic to a particular language or program verifier with a prototype implementation for C.}
}

GitHub Events

Total
  • Watch event: 2
  • Delete event: 3
  • Push event: 8
  • Pull request event: 3
  • Create event: 7
Last Year
  • Watch event: 2
  • Delete event: 3
  • Push event: 8
  • Pull request event: 3
  • Create event: 7

Issues and Pull Requests

Last synced: 7 months ago

All Time
  • Total issues: 0
  • Total pull requests: 1
  • Average time to close issues: N/A
  • Average time to close pull requests: about 5 hours
  • Total issue authors: 0
  • Total pull request authors: 1
  • Average comments per issue: 0
  • Average comments per pull request: 0.0
  • Merged pull requests: 1
  • Bot issues: 0
  • Bot pull requests: 0
Past Year
  • Issues: 0
  • Pull requests: 1
  • Average time to close issues: N/A
  • Average time to close pull requests: about 5 hours
  • Issue authors: 0
  • Pull request authors: 1
  • Average comments per issue: 0
  • Average comments per pull request: 0.0
  • Merged pull requests: 1
  • Bot issues: 0
  • Bot pull requests: 0
View more stats
Top Authors
Issue Authors
Pull Request Authors
  • ArquintL (3)
Top Labels
Issue Labels
Pull Request Labels

Packages

  • Total packages: 1
  • Total downloads: unknown
  • Total dependent packages: 0
  • Total dependent repositories: 1
  • Total versions: 1
proxy.golang.org: github.com/viperproject/ReusableProtocolVerificationLibrary
  • Versions: 1
  • Dependent Packages: 0
  • Dependent Repositories: 1
Rankings
Dependent repos count: 4.7%
Average: 7.1%
Dependent packages count: 9.6%
Last synced: 8 months ago

Dependencies

.github/workflows/library.yml actions
  • actions/checkout v3 composite
go.mod go
  • golang.org/x/crypto v0.0.0-20220722155217-630584e8d5aa
go.sum go
  • golang.org/x/crypto v0.0.0-20220722155217-630584e8d5aa
  • golang.org/x/net v0.0.0-20211112202133-69e39bad7dc2
  • golang.org/x/sys v0.0.0-20201119102817-f84b799fce68
  • golang.org/x/sys v0.0.0-20210423082822-04245dca01da
  • golang.org/x/sys v0.0.0-20210615035016-665e8c7367d1
  • golang.org/x/term v0.0.0-20201126162022-7de9c90e9dd1
  • golang.org/x/text v0.3.6
  • golang.org/x/tools v0.0.0-20180917221912-90fa682c2a6e