Binary-Compatible Verification of Filesystems with ACL2 Article Swipe

View

YOU? · · 2019 · Open Access · · DOI: https://doi.org/10.4230/lipics.itp.2019.25

Filesystems are an essential component of most computer systems. Work on the verification of filesystem functionality has been focused on constructing new filesystems in a manner which simplifies the process of verifying them against specifications. This leaves open the question of whether filesystems already in use are correct at the binary level. \nThis paper introduces LoFAT, a model of the FAT32 filesystem which efficiently implements a subset of the POSIX filesystem operations, and HiFAT, a more abstract model of FAT32 which is simpler to reason about. LoFAT is proved to be correct in terms of refinement of HiFAT, and made executable by enabling the state of the model to be written to and read from FAT32 disk images. EqFAT, an equivalence relation for disk images, considers whether two disk images contain the same directory tree modulo reordering of files and implementation-level details regarding cluster allocation. A suite of co-simulation tests uses EqFAT to compare the operation of existing FAT32 implementations to LoFAT and check the correctness of existing implementations of FAT32 such as the mtools suite of programs and the Linux FAT32 implementation. All models and proofs are formalized and mechanically verified in ACL2.

Related Topics

Concepts

Computer science Programming language Binary number Mathematics Arithmetic

Metadata

Type: article
Language: en
Landing Page: https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2019.25
OA Status: green
OpenAlex ID: https://openalex.org/W2953910293

All OpenAlex metadata

Raw OpenAlex JSON

OpenAlex ID: https://openalex.org/W2953910293

Canonical identifier for this work in OpenAlex
DOI: https://doi.org/10.4230/lipics.itp.2019.25

Digital Object Identifier
Title: Binary-Compatible Verification of Filesystems with ACL2

Work title
Type: article

OpenAlex work type
Language: en

Primary language
Publication year: 2019

Year of publication
Publication date: 2019-06-26

Full publication date if available
Authors: Mihir Parang Mehta, William R. Cook

List of authors in order
Landing page: https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2019.25

Publisher landing page
Open access: Yes

Whether a free full text is available
OA status: green

Open access status per OpenAlex
OA URL: https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2019.25

Direct OA link when available
Concepts: Computer science, Programming language, Binary number, Mathematics, Arithmetic

Top concepts (fields/topics) attached by OpenAlex
Cited by: 0

Total citation count in OpenAlex

Full payload

id	https://openalex.org/W2953910293
doi	https://doi.org/10.4230/lipics.itp.2019.25
ids.mag	2953910293
ids.openalex	https://openalex.org/W2953910293
fwci	0.0
type	article
title	Binary-Compatible Verification of Filesystems with ACL2
biblio.issue	141
biblio.volume
biblio.last_page
biblio.first_page
topics[0].id	https://openalex.org/T10904
topics[0].field.id	https://openalex.org/fields/17
topics[0].field.display_name	Computer Science
topics[0].score	0.9983000159263611
topics[0].domain.id	https://openalex.org/domains/3
topics[0].domain.display_name	Physical Sciences
topics[0].subfield.id	https://openalex.org/subfields/1708
topics[0].subfield.display_name	Hardware and Architecture
topics[0].display_name	Embedded Systems Design Techniques
topics[1].id	https://openalex.org/T10933
topics[1].field.id	https://openalex.org/fields/17
topics[1].field.display_name	Computer Science
topics[1].score	0.9970999956130981
topics[1].domain.id	https://openalex.org/domains/3
topics[1].domain.display_name	Physical Sciences
topics[1].subfield.id	https://openalex.org/subfields/1708
topics[1].subfield.display_name	Hardware and Architecture
topics[1].display_name	Real-Time Systems Scheduling
topics[2].id	https://openalex.org/T10054
topics[2].field.id	https://openalex.org/fields/17
topics[2].field.display_name	Computer Science
topics[2].score	0.9923999905586243
topics[2].domain.id	https://openalex.org/domains/3
topics[2].domain.display_name	Physical Sciences
topics[2].subfield.id	https://openalex.org/subfields/1708
topics[2].subfield.display_name	Hardware and Architecture
topics[2].display_name	Parallel Computing and Optimization Techniques
is_xpac	False
apc_list
apc_paid
concepts[0].id	https://openalex.org/C41008148
concepts[0].level	0
concepts[0].score	0.6563866138458252
concepts[0].wikidata	https://www.wikidata.org/wiki/Q21198
concepts[0].display_name	Computer science
concepts[1].id	https://openalex.org/C199360897
concepts[1].level	1
concepts[1].score	0.4686198830604553
concepts[1].wikidata	https://www.wikidata.org/wiki/Q9143
concepts[1].display_name	Programming language
concepts[2].id	https://openalex.org/C48372109
concepts[2].level	2
concepts[2].score	0.42029285430908203
concepts[2].wikidata	https://www.wikidata.org/wiki/Q3913
concepts[2].display_name	Binary number
concepts[3].id	https://openalex.org/C33923547
concepts[3].level	0
concepts[3].score	0.16414424777030945
concepts[3].wikidata	https://www.wikidata.org/wiki/Q395
concepts[3].display_name	Mathematics
concepts[4].id	https://openalex.org/C94375191
concepts[4].level	1
concepts[4].score	0.11428400874137878
concepts[4].wikidata	https://www.wikidata.org/wiki/Q11205
concepts[4].display_name	Arithmetic
keywords[0].id	https://openalex.org/keywords/computer-science
keywords[0].score	0.6563866138458252
keywords[0].display_name	Computer science
keywords[1].id	https://openalex.org/keywords/programming-language
keywords[1].score	0.4686198830604553
keywords[1].display_name	Programming language
keywords[2].id	https://openalex.org/keywords/binary-number
keywords[2].score	0.42029285430908203
keywords[2].display_name	Binary number
keywords[3].id	https://openalex.org/keywords/mathematics
keywords[3].score	0.16414424777030945
keywords[3].display_name	Mathematics
keywords[4].id	https://openalex.org/keywords/arithmetic
keywords[4].score	0.11428400874137878
keywords[4].display_name	Arithmetic
language	en
locations[0].id	pmh:oai:drops-oai.dagstuhl.de:11080
locations[0].is_oa	True
locations[0].source.id	https://openalex.org/S4306402524
locations[0].source.issn
locations[0].source.type	repository
locations[0].source.is_oa	False
locations[0].source.issn_l
locations[0].source.is_core	False
locations[0].source.is_in_doaj	False
locations[0].source.display_name	Leibniz-Zentrum für Informatik (Schloss Dagstuhl)
locations[0].source.host_organization	https://openalex.org/I2799853480
locations[0].source.host_organization_name	Schloss Dagstuhl – Leibniz Center for Informatics
locations[0].source.host_organization_lineage	https://openalex.org/I2799853480
locations[0].license	cc-by
locations[0].pdf_url
locations[0].version	publishedVersion
locations[0].raw_type	InProceedings
locations[0].license_id	https://openalex.org/licenses/cc-by
locations[0].is_accepted	True
locations[0].is_published	True
locations[0].raw_source_name
locations[0].landing_page_url	https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2019.25
locations[1].id	mag:2953910293
locations[1].is_oa	False
locations[1].source
locations[1].license
locations[1].pdf_url
locations[1].version
locations[1].raw_type
locations[1].license_id
locations[1].is_accepted	False
locations[1].is_published
locations[1].raw_source_name
locations[1].landing_page_url	https://drops.dagstuhl.de/opus/volltexte/2019/11080/pdf/LIPIcs-ITP-2019-25.pdf
authorships[0].author.id	https://openalex.org/A5063508735
authorships[0].author.orcid
authorships[0].author.display_name	Mihir Parang Mehta
authorships[0].author_position	first
authorships[0].raw_author_name	Mihir Parang Mehta
authorships[0].is_corresponding	False
authorships[1].author.id	https://openalex.org/A5029147559
authorships[1].author.orcid	https://orcid.org/0000-0003-4918-8975
authorships[1].author.display_name	William R. Cook
authorships[1].author_position	last
authorships[1].raw_author_name	William R. Cook
authorships[1].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://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2019.25
open_access.oa_status	green
open_access.any_repository_has_fulltext	False
created_date	2019-07-12T00:00:00
display_name	Binary-Compatible Verification of Filesystems with ACL2
has_fulltext	True
is_retracted	False
updated_date	2025-11-06T03:46:38.306776
primary_topic.id	https://openalex.org/T10904
primary_topic.field.id	https://openalex.org/fields/17
primary_topic.field.display_name	Computer Science
primary_topic.score	0.9983000159263611
primary_topic.domain.id	https://openalex.org/domains/3
primary_topic.domain.display_name	Physical Sciences
primary_topic.subfield.id	https://openalex.org/subfields/1708
primary_topic.subfield.display_name	Hardware and Architecture
primary_topic.display_name	Embedded Systems Design Techniques
cited_by_count	0
locations_count	2
best_oa_location.id	pmh:oai:drops-oai.dagstuhl.de:11080
best_oa_location.is_oa	True
best_oa_location.source.id	https://openalex.org/S4306402524
best_oa_location.source.issn
best_oa_location.source.type	repository
best_oa_location.source.is_oa	False
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	Leibniz-Zentrum für Informatik (Schloss Dagstuhl)
best_oa_location.source.host_organization	https://openalex.org/I2799853480
best_oa_location.source.host_organization_name	Schloss Dagstuhl – Leibniz Center for Informatics
best_oa_location.source.host_organization_lineage	https://openalex.org/I2799853480
best_oa_location.license	cc-by
best_oa_location.pdf_url
best_oa_location.version	publishedVersion
best_oa_location.raw_type	InProceedings
best_oa_location.license_id	https://openalex.org/licenses/cc-by
best_oa_location.is_accepted	True
best_oa_location.is_published	True
best_oa_location.raw_source_name
best_oa_location.landing_page_url	https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2019.25
primary_location.id	pmh:oai:drops-oai.dagstuhl.de:11080
primary_location.is_oa	True
primary_location.source.id	https://openalex.org/S4306402524
primary_location.source.issn
primary_location.source.type	repository
primary_location.source.is_oa	False
primary_location.source.issn_l
primary_location.source.is_core	False
primary_location.source.is_in_doaj	False
primary_location.source.display_name	Leibniz-Zentrum für Informatik (Schloss Dagstuhl)
primary_location.source.host_organization	https://openalex.org/I2799853480
primary_location.source.host_organization_name	Schloss Dagstuhl – Leibniz Center for Informatics
primary_location.source.host_organization_lineage	https://openalex.org/I2799853480
primary_location.license	cc-by
primary_location.pdf_url
primary_location.version	publishedVersion
primary_location.raw_type	InProceedings
primary_location.license_id	https://openalex.org/licenses/cc-by
primary_location.is_accepted	True
primary_location.is_published	True
primary_location.raw_source_name
primary_location.landing_page_url	https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2019.25
publication_date	2019-06-26
publication_year	2019
referenced_works_count	0
abstract_inverted_index.A	144
abstract_inverted_index.a	24, 55, 64, 73
abstract_inverted_index.an	2, 118
abstract_inverted_index.as	171
abstract_inverted_index.at	48
abstract_inverted_index.be	89, 108
abstract_inverted_index.by	100
abstract_inverted_index.in	23, 44, 91, 191
abstract_inverted_index.is	80, 86
abstract_inverted_index.of	5, 13, 30, 40, 57, 66, 77, 93, 95, 104, 136, 146, 155, 165, 168, 175
abstract_inverted_index.on	10, 19
abstract_inverted_index.to	82, 88, 107, 110, 151, 159
abstract_inverted_index.All	182
abstract_inverted_index.and	71, 97, 111, 138, 161, 177, 184, 188
abstract_inverted_index.are	1, 46, 186
abstract_inverted_index.for	121
abstract_inverted_index.has	16
abstract_inverted_index.new	21
abstract_inverted_index.the	11, 28, 38, 49, 58, 67, 102, 105, 130, 153, 163, 172, 178
abstract_inverted_index.two	126
abstract_inverted_index.use	45
abstract_inverted_index.This	35
abstract_inverted_index.Work	9
abstract_inverted_index.been	17
abstract_inverted_index.disk	115, 122, 127
abstract_inverted_index.from	113
abstract_inverted_index.made	98
abstract_inverted_index.more	74
abstract_inverted_index.most	6
abstract_inverted_index.open	37
abstract_inverted_index.read	112
abstract_inverted_index.same	131
abstract_inverted_index.such	170
abstract_inverted_index.them	32
abstract_inverted_index.tree	133
abstract_inverted_index.uses	149
abstract_inverted_index.ACL2.	192
abstract_inverted_index.EqFAT	150
abstract_inverted_index.FAT32	59, 78, 114, 157, 169, 180
abstract_inverted_index.Linux	179
abstract_inverted_index.LoFAT	85, 160
abstract_inverted_index.POSIX	68
abstract_inverted_index.check	162
abstract_inverted_index.files	137
abstract_inverted_index.model	56, 76, 106
abstract_inverted_index.paper	52
abstract_inverted_index.state	103
abstract_inverted_index.suite	145, 174
abstract_inverted_index.terms	92
abstract_inverted_index.tests	148
abstract_inverted_index.which	26, 61, 79
abstract_inverted_index.EqFAT,	117
abstract_inverted_index.HiFAT,	72, 96
abstract_inverted_index.LoFAT,	54
abstract_inverted_index.about.	84
abstract_inverted_index.binary	50
abstract_inverted_index.images	128
abstract_inverted_index.leaves	36
abstract_inverted_index.manner	25
abstract_inverted_index.models	183
abstract_inverted_index.modulo	134
abstract_inverted_index.mtools	173
abstract_inverted_index.proofs	185
abstract_inverted_index.proved	87
abstract_inverted_index.reason	83
abstract_inverted_index.subset	65
abstract_inverted_index.against	33
abstract_inverted_index.already	43
abstract_inverted_index.cluster	142
abstract_inverted_index.compare	152
abstract_inverted_index.contain	129
abstract_inverted_index.correct	47, 90
abstract_inverted_index.details	140
abstract_inverted_index.focused	18
abstract_inverted_index.images,	123
abstract_inverted_index.images.	116
abstract_inverted_index.process	29
abstract_inverted_index.simpler	81
abstract_inverted_index.whether	41, 125
abstract_inverted_index.written	109
abstract_inverted_index.abstract	75
abstract_inverted_index.computer	7
abstract_inverted_index.enabling	101
abstract_inverted_index.existing	156, 166
abstract_inverted_index.programs	176
abstract_inverted_index.question	39
abstract_inverted_index.relation	120
abstract_inverted_index.systems.	8
abstract_inverted_index.verified	190
abstract_inverted_index.component	4
abstract_inverted_index.considers	124
abstract_inverted_index.directory	132
abstract_inverted_index.essential	3
abstract_inverted_index.operation	154
abstract_inverted_index.regarding	141
abstract_inverted_index.verifying	31
abstract_inverted_index.executable	99
abstract_inverted_index.filesystem	14, 60, 69
abstract_inverted_index.formalized	187
abstract_inverted_index.implements	63
abstract_inverted_index.introduces	53
abstract_inverted_index.refinement	94
abstract_inverted_index.reordering	135
abstract_inverted_index.simplifies	27
abstract_inverted_index.Filesystems	0
abstract_inverted_index.allocation.	143
abstract_inverted_index.correctness	164
abstract_inverted_index.efficiently	62
abstract_inverted_index.equivalence	119
abstract_inverted_index.filesystems	22, 42
abstract_inverted_index.operations,	70
abstract_inverted_index.constructing	20
abstract_inverted_index.mechanically	189
abstract_inverted_index.verification	12
abstract_inverted_index.co-simulation	147
abstract_inverted_index.functionality	15
abstract_inverted_index.implementation.	181
abstract_inverted_index.implementations	158, 167
abstract_inverted_index.specifications.	34
abstract_inverted_index.level. \nThis	51
abstract_inverted_index.implementation-level	139
cited_by_percentile_year
countries_distinct_count	0
institutions_distinct_count	2
citation_normalized_percentile.value	0.06505744
citation_normalized_percentile.is_in_top_1_percent	False
citation_normalized_percentile.is_in_top_10_percent	False