Vault Filesystem implemented in the kernel of linux.
- Ada 71.4%
- Shell 12.4%
- C 10.4%
- Python 5.1%
- Makefile 0.7%
LowEel
423d941f47
Vfs_Seal builds and parses trusted.vaultfs.seal.G and the 80-byte plaintext its RSA-OAEP block wraps (key id, metadata key, data key); Vfs_Meta the metadata frame around AES-256-GCM and its records (key id, counter, created; unknown required types refused, optional ones skipped, order and lengths checked). Both are SPARK, proved. The OpenSSL layer gained RSA-OAEP with SHA-256, MGF1-SHA-256 and the label vaultfs-wrap-v1\0, and AES-256-GCM that wipes its output when the tag fails. Vfs_Keyfile opens a key file to seal with, every rule in order: place and modes for a given owner, protection, passphrase, RSA >= 4096 bits; vaultfs-keygen --check now uses it. Vfs_Namespace makes a new seal: fresh key id and keys from getrandom, wrapped with the public key, the metadata encrypted with the seal as associated data, secrets wiped. vaultfs-format --key KEYFILE --owner USER makes the root a namespace of generation 1: the device is checked first, then the key file (the owner's, passphrase asked), then marker, seal.1, meta.1 and last the control record trusted.vaultfs.active; owner USER, mode 0700. A wrong passphrase or another user's key leaves the volume untouched; a run interrupted after the marker is finished only with the same kind of root. testvectors/seal is made by openssl (the key file) and Python's cryptography (the wrap and the metadata); test_seal reads that seal and metadata end to end with the vector's key file and checks every fail-closed case: 41 checks. tests/vm/format_sealed.sh formats a sealed root in the VM and verify_root_seal.py opens it with Python's cryptography: fingerprints, real path, OAEP unwrap, key id, metadata under the seal as AAD, control record; plus the refusals. All host and VM tests pass; gnatprove proves 294 checks, none unproved. |
||
|---|---|---|
| include/uapi | ||
| kernel | ||
| LICENSES | ||
| systemd | ||
| tests | ||
| testvectors | ||
| tools | ||
| .gitignore | ||
| FORMAT.md | ||
| Makefile | ||
| MANUAL.md | ||
| README.md | ||
vaultfs
An encrypted filesystem for Linux where every directory is a vault of its own: a namespace with its own keys, opened with a key file and its passphrase, for your login session only. It is a kernel module stacked over a dedicated XFS volume, with userspace tools in Ada/SPARK.
- Contents are encrypted and authenticated (AES-256-GCM): tampering is detected, never read as data.
- A namespace can be opened while its parent stays closed; a closed one cannot be read or changed, by anyone, root included.
- Names and the tree's shape stay visible, by design.
- A vaultfs volume can only be mounted as vaultfs, never as plain XFS.
Status: design. Nothing here encrypts anything yet. The design is in
FORMAT.md (on-disk formats) and MANUAL.md (how the tools are used).
Layout
| Path | What | License |
|---|---|---|
kernel/ |
the module, C | GPL-2.0 |
include/uapi/ |
the interface shared by module and tools | GPL-2.0 WITH Linux-syscall-note |
tools/ |
the userspace tools, Ada/SPARK, C shim | EUPL-1.2 |
testvectors/ |
format test vectors shared by both sides | EUPL-1.2 |
tests/ |
VM and crash-consistency tests | EUPL-1.2 |
systemd/ |
the boot unit that rearms volumes | EUPL-1.2 |
FORMAT.md, MANUAL.md |
documentation | EUPL-1.2 |
Each file names its license in an SPDX-License-Identifier line; the texts
are in LICENSES/. The module is GPL-2.0 because the kernel interfaces it
needs are exported to GPL modules only.
Building
make kernel # kernel/vaultfs.ko for the running kernel (load it in a VM only)
make tools # tools/bin/, needs GNAT, gprbuild, libssl-dev, libkeyutils-dev
make test # the tools' unit tests, against testvectors/
make prove # the SPARK proofs of the tools
tests/vm/run.sh # the module in the test VM (tests/vm/README.md)
Target: Linux 7.0 and later, XFS V5, internal disks.