Protocols to Code: Formal Verification of a Next-Generation Internet Router Article Swipe
João C. Pereira
,
Tobias Klenze
,
Sofia Giampietro
,
Markus Limbeck
,
Dionysios Spiliopoulos
,
Felix A. Wolf
,
Marco Eilers
,
Christoph Sprenger
,
David Basin
,
Péter Müller
,
Adrian Perrig
·
YOU?
·
· 2024
· Open Access
·
· DOI: https://doi.org/10.48550/arxiv.2405.06074
YOU?
·
· 2024
· Open Access
·
· DOI: https://doi.org/10.48550/arxiv.2405.06074
We present the first formally-verified Internet router, which is part of the SCION Internet architecture. SCION routers run a cryptographic protocol for secure packet forwarding in an adversarial environment. We verify both the protocol's network-wide security properties and low-level properties of its implementation. More precisely, we develop a series of protocol models by refinement in Isabelle/HOL and we use an automated program verifier to prove that the router's Go code satisfies memory safety, crash freedom, freedom from data races, and adheres to the protocol model. Both verification efforts are soundly linked together. Our work demonstrates the feasibility of coherently verifying a critical network component from high-level protocol models down to performance-optimized production code, developed by an independent team. In the process, we uncovered critical bugs in both the protocol and its implementation, which were confirmed by the code developers, and we strengthened the protocol's security properties. This paper explains our approach, summarizes the main results, and distills lessons for the design and implementation of verifiable systems, for the handling of continuous changes, and for the verification techniques and tools employed.
Related Topics
Concepts
Metadata
- Type
- preprint
- Language
- en
- Landing Page
- http://arxiv.org/abs/2405.06074
- https://arxiv.org/pdf/2405.06074
- OA Status
- green
- Cited By
- 1
- Related Works
- 10
- OpenAlex ID
- https://openalex.org/W4396881719
All OpenAlex metadata
Raw OpenAlex JSON
- OpenAlex ID
-
https://openalex.org/W4396881719Canonical identifier for this work in OpenAlex
- DOI
-
https://doi.org/10.48550/arxiv.2405.06074Digital Object Identifier
- Title
-
Protocols to Code: Formal Verification of a Next-Generation Internet RouterWork title
- Type
-
preprintOpenAlex work type
- Language
-
enPrimary language
- Publication year
-
2024Year of publication
- Publication date
-
2024-05-09Full publication date if available
- Authors
-
João C. Pereira, Tobias Klenze, Sofia Giampietro, Markus Limbeck, Dionysios Spiliopoulos, Felix A. Wolf, Marco Eilers, Christoph Sprenger, David Basin, Péter Müller, Adrian PerrigList of authors in order
- Landing page
-
https://arxiv.org/abs/2405.06074Publisher landing page
- PDF URL
-
https://arxiv.org/pdf/2405.06074Direct link to full text PDF
- Open access
-
YesWhether a free full text is available
- OA status
-
greenOpen access status per OpenAlex
- OA URL
-
https://arxiv.org/pdf/2405.06074Direct OA link when available
- Concepts
-
Router, Computer science, Code (set theory), The Internet, Formal verification, Computer security, Computer network, Programming language, World Wide Web, Set (abstract data type)Top concepts (fields/topics) attached by OpenAlex
- Cited by
-
1Total citation count in OpenAlex
- Citations by year (recent)
-
2024: 1Per-year citation counts (last 5 years)
- Related works (count)
-
10Other works algorithmically related by OpenAlex
Full payload
| id | https://openalex.org/W4396881719 |
|---|---|
| doi | https://doi.org/10.48550/arxiv.2405.06074 |
| ids.doi | https://doi.org/10.48550/arxiv.2405.06074 |
| ids.openalex | https://openalex.org/W4396881719 |
| fwci | |
| type | preprint |
| title | Protocols to Code: Formal Verification of a Next-Generation Internet Router |
| biblio.issue | |
| biblio.volume | |
| biblio.last_page | |
| biblio.first_page | |
| topics[0].id | https://openalex.org/T11504 |
| topics[0].field.id | https://openalex.org/fields/17 |
| topics[0].field.display_name | Computer Science |
| topics[0].score | 0.9952999949455261 |
| topics[0].domain.id | https://openalex.org/domains/3 |
| topics[0].domain.display_name | Physical Sciences |
| topics[0].subfield.id | https://openalex.org/subfields/1705 |
| topics[0].subfield.display_name | Computer Networks and Communications |
| topics[0].display_name | Advanced Authentication Protocols Security |
| topics[1].id | https://openalex.org/T10142 |
| topics[1].field.id | https://openalex.org/fields/17 |
| topics[1].field.display_name | Computer Science |
| topics[1].score | 0.9821000099182129 |
| topics[1].domain.id | https://openalex.org/domains/3 |
| topics[1].domain.display_name | Physical Sciences |
| topics[1].subfield.id | https://openalex.org/subfields/1703 |
| topics[1].subfield.display_name | Computational Theory and Mathematics |
| topics[1].display_name | Formal Methods in Verification |
| topics[2].id | https://openalex.org/T10651 |
| topics[2].field.id | https://openalex.org/fields/22 |
| topics[2].field.display_name | Engineering |
| topics[2].score | 0.9789000153541565 |
| topics[2].domain.id | https://openalex.org/domains/3 |
| topics[2].domain.display_name | Physical Sciences |
| topics[2].subfield.id | https://openalex.org/subfields/2208 |
| topics[2].subfield.display_name | Electrical and Electronic Engineering |
| topics[2].display_name | IPv6, Mobility, Handover, Networks, Security |
| is_xpac | False |
| apc_list | |
| apc_paid | |
| concepts[0].id | https://openalex.org/C2775896111 |
| concepts[0].level | 2 |
| concepts[0].score | 0.6425391435623169 |
| concepts[0].wikidata | https://www.wikidata.org/wiki/Q642560 |
| concepts[0].display_name | Router |
| concepts[1].id | https://openalex.org/C41008148 |
| concepts[1].level | 0 |
| concepts[1].score | 0.5912966728210449 |
| concepts[1].wikidata | https://www.wikidata.org/wiki/Q21198 |
| concepts[1].display_name | Computer science |
| concepts[2].id | https://openalex.org/C2776760102 |
| concepts[2].level | 3 |
| concepts[2].score | 0.5901341438293457 |
| concepts[2].wikidata | https://www.wikidata.org/wiki/Q5139990 |
| concepts[2].display_name | Code (set theory) |
| concepts[3].id | https://openalex.org/C110875604 |
| concepts[3].level | 2 |
| concepts[3].score | 0.5405458807945251 |
| concepts[3].wikidata | https://www.wikidata.org/wiki/Q75 |
| concepts[3].display_name | The Internet |
| concepts[4].id | https://openalex.org/C111498074 |
| concepts[4].level | 2 |
| concepts[4].score | 0.4263990521430969 |
| concepts[4].wikidata | https://www.wikidata.org/wiki/Q173326 |
| concepts[4].display_name | Formal verification |
| concepts[5].id | https://openalex.org/C38652104 |
| concepts[5].level | 1 |
| concepts[5].score | 0.3902570605278015 |
| concepts[5].wikidata | https://www.wikidata.org/wiki/Q3510521 |
| concepts[5].display_name | Computer security |
| concepts[6].id | https://openalex.org/C31258907 |
| concepts[6].level | 1 |
| concepts[6].score | 0.35038667917251587 |
| concepts[6].wikidata | https://www.wikidata.org/wiki/Q1301371 |
| concepts[6].display_name | Computer network |
| concepts[7].id | https://openalex.org/C199360897 |
| concepts[7].level | 1 |
| concepts[7].score | 0.30542516708374023 |
| concepts[7].wikidata | https://www.wikidata.org/wiki/Q9143 |
| concepts[7].display_name | Programming language |
| concepts[8].id | https://openalex.org/C136764020 |
| concepts[8].level | 1 |
| concepts[8].score | 0.2313629686832428 |
| concepts[8].wikidata | https://www.wikidata.org/wiki/Q466 |
| concepts[8].display_name | World Wide Web |
| concepts[9].id | https://openalex.org/C177264268 |
| concepts[9].level | 2 |
| concepts[9].score | 0.0 |
| concepts[9].wikidata | https://www.wikidata.org/wiki/Q1514741 |
| concepts[9].display_name | Set (abstract data type) |
| keywords[0].id | https://openalex.org/keywords/router |
| keywords[0].score | 0.6425391435623169 |
| keywords[0].display_name | Router |
| keywords[1].id | https://openalex.org/keywords/computer-science |
| keywords[1].score | 0.5912966728210449 |
| keywords[1].display_name | Computer science |
| keywords[2].id | https://openalex.org/keywords/code |
| keywords[2].score | 0.5901341438293457 |
| keywords[2].display_name | Code (set theory) |
| keywords[3].id | https://openalex.org/keywords/the-internet |
| keywords[3].score | 0.5405458807945251 |
| keywords[3].display_name | The Internet |
| keywords[4].id | https://openalex.org/keywords/formal-verification |
| keywords[4].score | 0.4263990521430969 |
| keywords[4].display_name | Formal verification |
| keywords[5].id | https://openalex.org/keywords/computer-security |
| keywords[5].score | 0.3902570605278015 |
| keywords[5].display_name | Computer security |
| keywords[6].id | https://openalex.org/keywords/computer-network |
| keywords[6].score | 0.35038667917251587 |
| keywords[6].display_name | Computer network |
| keywords[7].id | https://openalex.org/keywords/programming-language |
| keywords[7].score | 0.30542516708374023 |
| keywords[7].display_name | Programming language |
| keywords[8].id | https://openalex.org/keywords/world-wide-web |
| keywords[8].score | 0.2313629686832428 |
| keywords[8].display_name | World Wide Web |
| language | en |
| locations[0].id | pmh:oai:arXiv.org:2405.06074 |
| locations[0].is_oa | True |
| locations[0].source.id | https://openalex.org/S4306400194 |
| locations[0].source.issn | |
| locations[0].source.type | repository |
| locations[0].source.is_oa | True |
| locations[0].source.issn_l | |
| locations[0].source.is_core | False |
| locations[0].source.is_in_doaj | False |
| locations[0].source.display_name | arXiv (Cornell University) |
| locations[0].source.host_organization | https://openalex.org/I205783295 |
| locations[0].source.host_organization_name | Cornell University |
| locations[0].source.host_organization_lineage | https://openalex.org/I205783295 |
| locations[0].license | |
| locations[0].pdf_url | https://arxiv.org/pdf/2405.06074 |
| locations[0].version | submittedVersion |
| locations[0].raw_type | |
| locations[0].license_id | |
| locations[0].is_accepted | False |
| locations[0].is_published | False |
| locations[0].raw_source_name | |
| locations[0].landing_page_url | http://arxiv.org/abs/2405.06074 |
| locations[1].id | doi:10.48550/arxiv.2405.06074 |
| locations[1].is_oa | True |
| locations[1].source.id | https://openalex.org/S4306400194 |
| locations[1].source.issn | |
| locations[1].source.type | repository |
| locations[1].source.is_oa | True |
| locations[1].source.issn_l | |
| locations[1].source.is_core | False |
| locations[1].source.is_in_doaj | False |
| locations[1].source.display_name | arXiv (Cornell University) |
| locations[1].source.host_organization | https://openalex.org/I205783295 |
| locations[1].source.host_organization_name | Cornell University |
| locations[1].source.host_organization_lineage | https://openalex.org/I205783295 |
| locations[1].license | |
| locations[1].pdf_url | |
| locations[1].version | |
| locations[1].raw_type | article |
| locations[1].license_id | |
| locations[1].is_accepted | False |
| locations[1].is_published | |
| locations[1].raw_source_name | |
| locations[1].landing_page_url | https://doi.org/10.48550/arxiv.2405.06074 |
| indexed_in | arxiv, datacite |
| authorships[0].author.id | https://openalex.org/A5103031260 |
| authorships[0].author.orcid | https://orcid.org/0000-0003-4671-4132 |
| authorships[0].author.display_name | João C. Pereira |
| authorships[0].author_position | first |
| authorships[0].raw_author_name | Pereira, João C. |
| authorships[0].is_corresponding | False |
| authorships[1].author.id | https://openalex.org/A5041880436 |
| authorships[1].author.orcid | https://orcid.org/0000-0002-6505-3942 |
| authorships[1].author.display_name | Tobias Klenze |
| authorships[1].author_position | middle |
| authorships[1].raw_author_name | Klenze, Tobias |
| authorships[1].is_corresponding | False |
| authorships[2].author.id | https://openalex.org/A5014532120 |
| authorships[2].author.orcid | https://orcid.org/0009-0004-9628-0007 |
| authorships[2].author.display_name | Sofia Giampietro |
| authorships[2].author_position | middle |
| authorships[2].raw_author_name | Giampietro, Sofia |
| authorships[2].is_corresponding | False |
| authorships[3].author.id | https://openalex.org/A5098060218 |
| authorships[3].author.orcid | https://orcid.org/0009-0007-2805-6945 |
| authorships[3].author.display_name | Markus Limbeck |
| authorships[3].author_position | middle |
| authorships[3].raw_author_name | Limbeck, Markus |
| authorships[3].is_corresponding | False |
| authorships[4].author.id | https://openalex.org/A5098034918 |
| authorships[4].author.orcid | |
| authorships[4].author.display_name | Dionysios Spiliopoulos |
| authorships[4].author_position | middle |
| authorships[4].raw_author_name | Spiliopoulos, Dionysios |
| authorships[4].is_corresponding | False |
| authorships[5].author.id | https://openalex.org/A5085816785 |
| authorships[5].author.orcid | https://orcid.org/0000-0002-8573-2387 |
| authorships[5].author.display_name | Felix A. Wolf |
| authorships[5].author_position | middle |
| authorships[5].raw_author_name | Wolf, Felix A. |
| authorships[5].is_corresponding | False |
| authorships[6].author.id | https://openalex.org/A5046632033 |
| authorships[6].author.orcid | https://orcid.org/0000-0003-4891-6950 |
| authorships[6].author.display_name | Marco Eilers |
| authorships[6].author_position | middle |
| authorships[6].raw_author_name | Eilers, Marco |
| authorships[6].is_corresponding | False |
| authorships[7].author.id | https://openalex.org/A5037740498 |
| authorships[7].author.orcid | https://orcid.org/0000-0003-2941-5165 |
| authorships[7].author.display_name | Christoph Sprenger |
| authorships[7].author_position | middle |
| authorships[7].raw_author_name | Sprenger, Christoph |
| authorships[7].is_corresponding | False |
| authorships[8].author.id | https://openalex.org/A5025344654 |
| authorships[8].author.orcid | https://orcid.org/0000-0003-2952-939X |
| authorships[8].author.display_name | David Basin |
| authorships[8].author_position | middle |
| authorships[8].raw_author_name | Basin, David |
| authorships[8].is_corresponding | False |
| authorships[9].author.id | https://openalex.org/A5073853337 |
| authorships[9].author.orcid | https://orcid.org/0000-0001-7001-2566 |
| authorships[9].author.display_name | Péter Müller |
| authorships[9].author_position | middle |
| authorships[9].raw_author_name | Müller, Peter |
| authorships[9].is_corresponding | False |
| authorships[10].author.id | https://openalex.org/A5056518136 |
| authorships[10].author.orcid | https://orcid.org/0000-0002-5280-5412 |
| authorships[10].author.display_name | Adrian Perrig |
| authorships[10].author_position | last |
| authorships[10].raw_author_name | Perrig, Adrian |
| authorships[10].is_corresponding | False |
| has_content.pdf | False |
| has_content.grobid_xml | False |
| is_paratext | False |
| open_access.is_oa | True |
| open_access.oa_url | https://arxiv.org/pdf/2405.06074 |
| open_access.oa_status | green |
| open_access.any_repository_has_fulltext | False |
| created_date | 2025-10-10T00:00:00 |
| display_name | Protocols to Code: Formal Verification of a Next-Generation Internet Router |
| has_fulltext | False |
| is_retracted | False |
| updated_date | 2025-11-06T06:51:31.235846 |
| primary_topic.id | https://openalex.org/T11504 |
| primary_topic.field.id | https://openalex.org/fields/17 |
| primary_topic.field.display_name | Computer Science |
| primary_topic.score | 0.9952999949455261 |
| primary_topic.domain.id | https://openalex.org/domains/3 |
| primary_topic.domain.display_name | Physical Sciences |
| primary_topic.subfield.id | https://openalex.org/subfields/1705 |
| primary_topic.subfield.display_name | Computer Networks and Communications |
| primary_topic.display_name | Advanced Authentication Protocols Security |
| related_works | https://openalex.org/W2122026593, https://openalex.org/W2582203024, https://openalex.org/W1588358165, https://openalex.org/W4237683758, https://openalex.org/W2370711413, https://openalex.org/W2052038519, https://openalex.org/W2375932043, https://openalex.org/W2841075164, https://openalex.org/W1980506749, https://openalex.org/W2375594474 |
| cited_by_count | 1 |
| counts_by_year[0].year | 2024 |
| counts_by_year[0].cited_by_count | 1 |
| locations_count | 2 |
| best_oa_location.id | pmh:oai:arXiv.org:2405.06074 |
| best_oa_location.is_oa | True |
| best_oa_location.source.id | https://openalex.org/S4306400194 |
| best_oa_location.source.issn | |
| best_oa_location.source.type | repository |
| best_oa_location.source.is_oa | True |
| best_oa_location.source.issn_l | |
| best_oa_location.source.is_core | False |
| best_oa_location.source.is_in_doaj | False |
| best_oa_location.source.display_name | arXiv (Cornell University) |
| best_oa_location.source.host_organization | https://openalex.org/I205783295 |
| best_oa_location.source.host_organization_name | Cornell University |
| best_oa_location.source.host_organization_lineage | https://openalex.org/I205783295 |
| best_oa_location.license | |
| best_oa_location.pdf_url | https://arxiv.org/pdf/2405.06074 |
| best_oa_location.version | submittedVersion |
| best_oa_location.raw_type | |
| best_oa_location.license_id | |
| best_oa_location.is_accepted | False |
| best_oa_location.is_published | False |
| best_oa_location.raw_source_name | |
| best_oa_location.landing_page_url | http://arxiv.org/abs/2405.06074 |
| primary_location.id | pmh:oai:arXiv.org:2405.06074 |
| primary_location.is_oa | True |
| primary_location.source.id | https://openalex.org/S4306400194 |
| primary_location.source.issn | |
| primary_location.source.type | repository |
| primary_location.source.is_oa | True |
| primary_location.source.issn_l | |
| primary_location.source.is_core | False |
| primary_location.source.is_in_doaj | False |
| primary_location.source.display_name | arXiv (Cornell University) |
| primary_location.source.host_organization | https://openalex.org/I205783295 |
| primary_location.source.host_organization_name | Cornell University |
| primary_location.source.host_organization_lineage | https://openalex.org/I205783295 |
| primary_location.license | |
| primary_location.pdf_url | https://arxiv.org/pdf/2405.06074 |
| primary_location.version | submittedVersion |
| primary_location.raw_type | |
| primary_location.license_id | |
| primary_location.is_accepted | False |
| primary_location.is_published | False |
| primary_location.raw_source_name | |
| primary_location.landing_page_url | http://arxiv.org/abs/2405.06074 |
| publication_date | 2024-05-09 |
| publication_year | 2024 |
| referenced_works_count | 0 |
| abstract_inverted_index.a | 18, 47, 100 |
| abstract_inverted_index.Go | 68 |
| abstract_inverted_index.In | 118 |
| abstract_inverted_index.We | 0, 29 |
| abstract_inverted_index.an | 26, 59, 115 |
| abstract_inverted_index.by | 52, 114, 135 |
| abstract_inverted_index.in | 25, 54, 125 |
| abstract_inverted_index.is | 8 |
| abstract_inverted_index.of | 10, 40, 49, 97, 163, 169 |
| abstract_inverted_index.to | 63, 81, 109 |
| abstract_inverted_index.we | 45, 57, 121, 140 |
| abstract_inverted_index.Our | 92 |
| abstract_inverted_index.and | 37, 56, 79, 129, 139, 155, 161, 172, 177 |
| abstract_inverted_index.are | 88 |
| abstract_inverted_index.for | 21, 158, 166, 173 |
| abstract_inverted_index.its | 41, 130 |
| abstract_inverted_index.our | 149 |
| abstract_inverted_index.run | 17 |
| abstract_inverted_index.the | 2, 11, 32, 66, 82, 95, 119, 127, 136, 142, 152, 159, 167, 174 |
| abstract_inverted_index.use | 58 |
| abstract_inverted_index.Both | 85 |
| abstract_inverted_index.More | 43 |
| abstract_inverted_index.This | 146 |
| abstract_inverted_index.both | 31, 126 |
| abstract_inverted_index.bugs | 124 |
| abstract_inverted_index.code | 69, 137 |
| abstract_inverted_index.data | 77 |
| abstract_inverted_index.down | 108 |
| abstract_inverted_index.from | 76, 104 |
| abstract_inverted_index.main | 153 |
| abstract_inverted_index.part | 9 |
| abstract_inverted_index.that | 65 |
| abstract_inverted_index.were | 133 |
| abstract_inverted_index.work | 93 |
| abstract_inverted_index.SCION | 12, 15 |
| abstract_inverted_index.code, | 112 |
| abstract_inverted_index.crash | 73 |
| abstract_inverted_index.first | 3 |
| abstract_inverted_index.paper | 147 |
| abstract_inverted_index.prove | 64 |
| abstract_inverted_index.team. | 117 |
| abstract_inverted_index.tools | 178 |
| abstract_inverted_index.which | 7, 132 |
| abstract_inverted_index.design | 160 |
| abstract_inverted_index.linked | 90 |
| abstract_inverted_index.memory | 71 |
| abstract_inverted_index.model. | 84 |
| abstract_inverted_index.models | 51, 107 |
| abstract_inverted_index.packet | 23 |
| abstract_inverted_index.races, | 78 |
| abstract_inverted_index.secure | 22 |
| abstract_inverted_index.series | 48 |
| abstract_inverted_index.verify | 30 |
| abstract_inverted_index.adheres | 80 |
| abstract_inverted_index.develop | 46 |
| abstract_inverted_index.efforts | 87 |
| abstract_inverted_index.freedom | 75 |
| abstract_inverted_index.lessons | 157 |
| abstract_inverted_index.network | 102 |
| abstract_inverted_index.present | 1 |
| abstract_inverted_index.program | 61 |
| abstract_inverted_index.router, | 6 |
| abstract_inverted_index.routers | 16 |
| abstract_inverted_index.safety, | 72 |
| abstract_inverted_index.soundly | 89 |
| abstract_inverted_index.Internet | 5, 13 |
| abstract_inverted_index.changes, | 171 |
| abstract_inverted_index.critical | 101, 123 |
| abstract_inverted_index.distills | 156 |
| abstract_inverted_index.explains | 148 |
| abstract_inverted_index.freedom, | 74 |
| abstract_inverted_index.handling | 168 |
| abstract_inverted_index.process, | 120 |
| abstract_inverted_index.protocol | 20, 50, 83, 106, 128 |
| abstract_inverted_index.results, | 154 |
| abstract_inverted_index.router's | 67 |
| abstract_inverted_index.security | 35, 144 |
| abstract_inverted_index.systems, | 165 |
| abstract_inverted_index.verifier | 62 |
| abstract_inverted_index.approach, | 150 |
| abstract_inverted_index.automated | 60 |
| abstract_inverted_index.component | 103 |
| abstract_inverted_index.confirmed | 134 |
| abstract_inverted_index.developed | 113 |
| abstract_inverted_index.employed. | 179 |
| abstract_inverted_index.low-level | 38 |
| abstract_inverted_index.satisfies | 70 |
| abstract_inverted_index.together. | 91 |
| abstract_inverted_index.uncovered | 122 |
| abstract_inverted_index.verifying | 99 |
| abstract_inverted_index.coherently | 98 |
| abstract_inverted_index.continuous | 170 |
| abstract_inverted_index.forwarding | 24 |
| abstract_inverted_index.high-level | 105 |
| abstract_inverted_index.precisely, | 44 |
| abstract_inverted_index.production | 111 |
| abstract_inverted_index.properties | 36, 39 |
| abstract_inverted_index.protocol's | 33, 143 |
| abstract_inverted_index.refinement | 53 |
| abstract_inverted_index.summarizes | 151 |
| abstract_inverted_index.techniques | 176 |
| abstract_inverted_index.verifiable | 164 |
| abstract_inverted_index.adversarial | 27 |
| abstract_inverted_index.developers, | 138 |
| abstract_inverted_index.feasibility | 96 |
| abstract_inverted_index.independent | 116 |
| abstract_inverted_index.properties. | 145 |
| abstract_inverted_index.Isabelle/HOL | 55 |
| abstract_inverted_index.demonstrates | 94 |
| abstract_inverted_index.environment. | 28 |
| abstract_inverted_index.network-wide | 34 |
| abstract_inverted_index.strengthened | 141 |
| abstract_inverted_index.verification | 86, 175 |
| abstract_inverted_index.architecture. | 14 |
| abstract_inverted_index.cryptographic | 19 |
| abstract_inverted_index.implementation | 162 |
| abstract_inverted_index.implementation, | 131 |
| abstract_inverted_index.implementation. | 42 |
| abstract_inverted_index.formally-verified | 4 |
| abstract_inverted_index.performance-optimized | 110 |
| cited_by_percentile_year | |
| countries_distinct_count | 0 |
| institutions_distinct_count | 11 |
| citation_normalized_percentile |