
> Note: I have a similar [setup on Arch](https://docs.gassmann.dev/docs/category/arch) and was annoyed by how different things were on Proxmox/Debian. I'm currently running the below on my four-node Proxmox cluster with no issues.

Proxmox currently lacks a good way of having full-disk encryption with TPM unlock, along with a fully verified boot chain with secure boot. This is unfortunate, especially for a cluster where you'll store lots of personal data. I therefore wanted to find a way of replicating my Arch setup on Proxmox as well (I really wish I could run Proxmox on Arch).

My goals:

- db holds only my key (no shim, no MOK)
- one signed UKI, booted directly by firmware, no bootloader
- TPM unseals the LUKS root on PCR 7 (stable across kernel updates)
- minimal changes to Debian and Proxmox

Grab all files:

```bash
BASE=https://thomasgassmann.com/static/blog/proxmox-verified-boot
mkdir -p bin etc/kernel/{postinst.d,postrm.d} etc/initramfs/post-update.d etc/initramfs-tools/{hooks,scripts/init-premount} sbin
curl -fSL "$BASE/install.sh"                                            -o install.sh
curl -fSL "$BASE/etc/kernel/uki.conf"                                   -o etc/kernel/uki.conf
curl -fSL "$BASE/sbin/pve-uki-update"                                   -o sbin/pve-uki-update
curl -fSL "$BASE/etc/kernel/postinst.d/zz-pve-uki"                      -o etc/kernel/postinst.d/zz-pve-uki
curl -fSL "$BASE/etc/kernel/postrm.d/zz-pve-uki"                        -o etc/kernel/postrm.d/zz-pve-uki
curl -fSL "$BASE/etc/initramfs/post-update.d/zz-pve-uki"                -o etc/initramfs/post-update.d/zz-pve-uki
curl -fSL "$BASE/etc/initramfs-tools/hooks/tpm2-cryptsetup"             -o etc/initramfs-tools/hooks/tpm2-cryptsetup
curl -fSL "$BASE/etc/initramfs-tools/scripts/init-premount/tpm2-unlock" -o etc/initramfs-tools/scripts/init-premount/tpm2-unlock
curl -fSL "$BASE/bin/gen-keys.sh"                                       -o bin/gen-keys.sh
curl -fSL "$BASE/bin/enroll-keys.sh"                                    -o bin/enroll-keys.sh
curl -fSL "$BASE/bin/verify.sh"                                         -o bin/verify.sh
chmod +x install.sh sbin/pve-uki-update bin/*.sh
```

## Boot chain

```
UEFI (my PK/KEK; db = my key only)
  -> EFI/PVE/current.efi        UKI signed with my db key
     -> systemd-stub -> PVE kernel + initramfs-tools initrd
        -> tpm2-unlock: systemd-cryptsetup attach (TPM2, PCR 7), else passphrase
           -> LVM -> encrypted root -> Proxmox VE
```

db holds only my key. PCR 7 records which cert verified the chain, so a foreign signed image
can never unseal the key.

`proxmox-boot-tool` only activates when `/etc/kernel/proxmox-boot-uuids`
exists, which it does not on ext4/LVM, so it stays inert.

## The files

- [install.sh](/static/blog/proxmox-verified-boot/install.sh): installs
  packages and deploys hooks. Inert until keys exist.
- [etc/kernel/uki.conf](/static/blog/proxmox-verified-boot/etc/kernel/uki.conf):
  ukify config. Signs the UKI with the db key, no PCR signing.
- [sbin/pve-uki-update](/static/blog/proxmox-verified-boot/sbin/pve-uki-update):
  builds and signs the UKI, rotates current.efi to previous.efi on version
  change, creates two EFI boot entries once. The three hooks call it.
- [etc/kernel/postinst.d/zz-pve-uki](/static/blog/proxmox-verified-boot/etc/kernel/postinst.d/zz-pve-uki),
  [postrm.d/zz-pve-uki](/static/blog/proxmox-verified-boot/etc/kernel/postrm.d/zz-pve-uki),
  [initramfs/post-update.d/zz-pve-uki](/static/blog/proxmox-verified-boot/etc/initramfs/post-update.d/zz-pve-uki):
  one line hooks that run pve-uki-update on kernel or initrd change.
- [etc/initramfs-tools/hooks/tpm2-cryptsetup](/static/blog/proxmox-verified-boot/etc/initramfs-tools/hooks/tpm2-cryptsetup):
  puts systemd-cryptsetup, the libcryptsetup TPM2 token plugin, and TSS
  libraries into the initrd. The token plugin is what Debian's
  cryptsetup-initramfs leaves out.
- [etc/initramfs-tools/scripts/init-premount/tpm2-unlock](/static/blog/proxmox-verified-boot/etc/initramfs-tools/scripts/init-premount/tpm2-unlock):
  attaches each LUKS device with the PCR 7 policy before cryptsetup's own
  script runs. On failure it exits cleanly so the passphrase prompt fires.
- [bin/gen-keys.sh](/static/blog/proxmox-verified-boot/bin/gen-keys.sh):
  one time PK, KEK and db key generation.
- [bin/enroll-keys.sh](/static/blog/proxmox-verified-boot/bin/enroll-keys.sh):
  enrolls db, then KEK, then PK. Order matters: writing PK last leaves Setup
  Mode and locks the store.
- [bin/verify.sh](/static/blog/proxmox-verified-boot/bin/verify.sh): read
  only health check. Run after each step.

## Runbook

Order matters. The UKI boot path is proven first while the disk is unencrypted
and every step is reversible. Only then encrypt.

Reference layout after a normal Proxmox ISO install on a single NVMe:

```
nvme0n1p1   1M    BIOS boot (unused under UEFI)
nvme0n1p2   1G    ESP, mounted /boot/efi
nvme0n1p3   rest  LVM PV -> VG pve: swap, root (holds /boot), data thin pool
```

Replace `/dev/nvme0n1p3` with your own PV throughout; a wrong device name in
the encrypt step destroys data.

The ISO puts `/boot` inside the root LV. After encryption GRUB can no longer
read it, so the signed UKI becomes the only boot path. Rescue means a live
ISO plus passphrase plus chroot.

### Step 0: firmware

Enable TPM 2.0 and clear it. Set a firmware administrator password (protects
the Secure Boot toggle and key store). Leave Secure Boot off. Confirm the
firmware can reset the Secure Boot key store to Setup Mode.

### Step 1: preconditions

```bash
efibootmgr -v                    # must show UEFI boot entries (not legacy BIOS)
ls /etc/kernel/proxmox-boot-uuids 2>/dev/null \
    || echo "proxmox-boot-tool inert (expected on ext4/LVM)"
vgs pve
pvdisplay --maps /dev/nvme0n1p3  # LAST segment must be FREE (>= 16 MiB)
```

If the PV tail is allocated, `pvmove` the tail extents first.

### Step 2: install the tooling

```bash
./install.sh
apt install cryptsetup cryptsetup-initramfs
```

### Step 3: keys and first UKI, Secure Boot still off

```bash
bin/gen-keys.sh
```

Back up `/etc/kernel/pve-uki/` (private keys) and a LUKS header backup to
offline storage. Then build the first UKI:

```bash
/usr/local/sbin/pve-uki-update
```

Reboot, pick the `Proxmox VE` entry from the firmware boot menu (or
`efibootmgr --bootnext`), run `bin/verify.sh`. Expect a stub boot, matching
cmdline, valid signature. Secure Boot reports disabled here, which is correct.

### Step 4: enroll keys, enable Secure Boot

Reboot into firmware setup, reset Secure Boot key store to Setup Mode, boot
back into Proxmox:

```bash
bin/enroll-keys.sh
```

If the firmware refuses efivar writes, copy `enroll/{db,KEK,PK}.auth` to a
FAT USB stick and enroll through the firmware UI in that order. Reboot into
firmware setup, enable Secure Boot, boot the `Proxmox VE` entry, run
`bin/verify.sh`.

Now that Secure Boot is on with only your key in db, the Microsoft-signed shim
the ISO installed is no longer trusted, and its package hook throws a red "No
valid UEFI Secure Boot signatures found ... FATAL ERROR" dialog on the next
apt run. You boot the UKI directly, not shim, so it is harmless. Remove the
shim and MOK stack you no longer use so it stops recurring (packages that are
not installed are skipped):

```bash
apt purge shim-signed shim-helpers-amd64-signed mokutil proxmox-secure-boot-support
apt --fix-broken install   # configures anything the failing shim hook left half-done
```

Do not add `--autoremove` or list `grub-efi-amd64-signed`: apt protects the
signed GRUB as a boot package and aborts the whole removal. Leaving it
installed is fine, it is simply unused.

GRUB still recommends shim, so a later `apt full-upgrade` can pull it back and
re-trigger the dialog. Block it permanently with a negative apt pin:

```bash
cat > /etc/apt/preferences.d/no-shim.pref <<'EOF'
Package: shim-signed shim-signed-common shim-helpers-amd64-signed mokutil
Pin: release *
Pin-Priority: -1
EOF
```

### Step 5: make room for the LUKS header

`cryptsetup reencrypt --encrypt` writes its LUKS2 header at the front of the
partition and shifts data down. LUKS2 default header is 16 MiB. Shrink the PV:

```bash
SIZE=$(pvs --noheadings --units b --nosuffix -o pv_size /dev/nvme0n1p3 | tr -d ' ')
pvresize --setphysicalvolumesize $((SIZE - 16777216))B /dev/nvme0n1p3
```

`pvresize` refuses if tail extents are in use. Resolve with `pvmove`, never
force.

### Step 6: encrypt in place, from a live ISO

Boot a live ISO with recent cryptsetup (e.g. Arch). This rewrites the whole
partition and is the one irreversible step. Back up first: an interrupted
reencrypt or a wrong device name can destroy data.

You may need to disable secure boot again for this temporarily.

```bash
vgchange -an pve
cryptsetup reencrypt --encrypt --reduce-device-size 16M /dev/nvme0n1p3
    # 16 MiB = LUKS2 default header; choose the permanent fallback passphrase

cryptsetup open /dev/nvme0n1p3 cryptlvm
vgchange -ay pve
mount /dev/pve/root /mnt
mount /dev/nvme0n1p2 /mnt/boot/efi
arch-chroot /mnt
```

Inside the chroot:

```bash
export PATH="$PATH:/usr/sbin"
echo "cryptlvm UUID=$(blkid -s UUID -o value /dev/nvme0n1p3) none luks,discard" >> /etc/crypttab
update-initramfs -u -k all
ls -l /boot/efi/EFI/PVE/          # current.efi must be freshly rebuilt
exit
reboot
```

The kernel cmdline does not change: `root=/dev/mapper/pve-root` is the same
LV name, now on top of LUKS. The `update-initramfs` pulls in cryptroot and
the TPM2 unlock pieces, and the post-update hook rebuilds and re-signs the UKI.
The `discard` in the crypttab line enables TRIM passthrough, which leaks
used-vs-free block patterns; drop it if that matters.

First boot prompts for the LUKS passphrase (TPM not enrolled yet). That
working prompt is the fallback path test.

Optionally reclaim LVM extent rounding slack:

```bash
pvresize /dev/mapper/cryptlvm
```

### Step 7: TPM enrollment, PCR 7

Re-enable Secure Boot if the live ISO left it off. Then bind the LUKS key to
PCR 7:

```bash
systemd-cryptenroll --tpm2-device=auto --tpm2-pcrs=7 /dev/nvme0n1p3
reboot
```

PCR 7 is Secure Boot state plus the db cert. Stable across kernel updates and
boot entry changes. Never remove the passphrase keyslot.

The reboot should reach the login prompt with no passphrase. `bin/verify.sh`
prints `last boot unlocked the root via TPM2 (no passphrase)`.

### Step 8: prove it survives updates

```bash
apt install --reinstall proxmox-kernel-$(uname -r)   # then reboot
```

Hooks rebuild and re-sign `current.efi`, `previous.efi` appears, reboot auto
unlocks. Test the failure path: disable Secure Boot once, watch TPM refuse and
passphrase prompt appear, re-enable, confirm auto unlock returns.

## Result

`bin/verify.sh` is green: Secure Boot on with your own keys, signed UKI, LUKS root unsealed from TPM on PCR 7 with
passphrase as fallback.

Verified boot for Proxmox VE


This semester, I'll be teaching the course "Einführung in die Programmierung" (Introduction to Programming) at ETH Zürich. One idea that has been on my mind for quite some time is to create an EBNF verifier, along with an editor that provides basic EBNF language support. Given that I've already been working with it a few years ago, I decided to use Monaco editor, Microsoft's web-based editor, which also powers Visual Studio Code.

> You can find the editor at [gassmann.dev/ebnf](/ebnf).

*Note: Much of the grammar simplification and the details of the CYK algorithm have been adapted from [github.com/JM4ier/parsley](https://github.com/JM4ier/parsley).*

## Syntax

The EBNF parser mostly follows the EBNF syntax as discussed in the "Einführung in die Programmierung" course taught at ETH Zürich. Some things to be aware of include:

- The input is evaluated against the **last** rule
- Each EBNF rule occupies exactly one line
- Comments can be created using `#`
- Empty lines are skipped
- Sequences bind stronger than selections, i.e. `<r> <= [+|-] 0|2|4|6|8` is interpreted as `<r> <= ([+|-] 0)|2|4|6|8` and not as `<r> <= [+|-] (0|2|4|6|8)`. This also coincides with the rules of the lecture, see [slide 10 of this document](https://ethz.ch/content/dam/ethz/special-interest/infk/inst-cs/lst-dam/documents/Education/Classes/Fall2023/0027_Intro/Slides/01B_ebnf_23.pdf). Always set parentheses to avoid confusion.
- You won't be able to use `ε` to match an empty sequence, use `""` instead. The following rule matches the empty string:
  ```bnf
  <empty> <= ""
  ```

The tool consists of an EBNF verifier and an EBNF producer. The verifier checks if a given input conforms to the defined EBNF rules, while the producer generates words based on the rules, incrementally increasing their length.

## Verify

The verifier provides a simple editor where you can input text to validate against the EBNF rules. Each line in the lower half is evaluated against the EBNF ruleset separately. If a line matches the EBNF ruleset, the line is highlighted green, if a line does not match the EBNF ruleset, the line is highlighted red.

You can try the EBNF verifier down below with the EBNF rules from the [HS22 exam](https://exams.vis.ethz.ch/exams/e2r7jb0u.pdf#zjzj01o1yy7lyfqr):

<EbnfBlogWrapper initialRules={`
<identifier> <= a | b | y | z | 7 | x | c | k | m | n

<unary_expression> <= <unary_operator> <primary_expression>
<postfix_expression> <= <primary_expression> | <postfix_expression> ++ | <postfix_expression> --
<primary_expression> <= "(" <special_expression> ")" | <identifier>
<unary_operator> <= * | !
<assignment_expression> <= <expression>" "<assignment_operator>" "<special_expression>
<assignment_operator> <= = | +=
<special_expression> <= <primary_expression> | <special_expression>" "<binary_operator>" "<expression>
<binary_operator> <= * | / | + | %
<expression> <= <assignment_expression> | <postfix_expression> | <unary_expression>
`.trim()} initialContent={`
*(a + b)
z = *(a + b)
y += (z / 7)
x = (a = b)
(b++) += ((a + c))
a = (*b * *c)
y++ * 7
k = m = n
`.trim()} height={'250px'} initialTab={'verify'} />

Note that this EBNF verifier is whitespace-sensitive. For instance, the EBNF ruleset above matches expressions like `*(a + b)` but not `*(a+b)`. To faciliate things, you might consider adding a rule akin to `<whitespace> <= {" "}`.

With an additional `whitespace` rule as suggested above, we'd have a ruleset similar to the one below (which now also matches `*(a+b)`):

<EbnfBlogWrapper initialRules={`
<identifier> <= a | b | y | z | 7 | x | c | k | m | n

<whitespace> <= {" "}
<unary_expression> <= <unary_operator> <primary_expression>
<postfix_expression> <= <primary_expression> | <postfix_expression> ++ | <postfix_expression> --
<primary_expression> <= "(" <special_expression> ")" | <identifier>
<unary_operator> <= * | !
<assignment_expression> <= <expression> <whitespace> <assignment_operator> <whitespace> <special_expression>
<assignment_operator> <= = | +=
<special_expression> <= <primary_expression> | <special_expression> <whitespace> <binary_operator> <whitespace> <expression>
<binary_operator> <= * | / | + | %
<expression> <= <assignment_expression> | <postfix_expression> | <unary_expression>
`.trim()} initialContent={`
*(a + b)
*(a+b)
z = *(a + b)
z=*(a+b)
y += (z / 7)
y+=(z/7)
x = (a = b)
x=(a=b)
(b++) += ((a + c))
(b++)+=((a+c))
a = (*b * *c)
a=(*b**c)
y++ * 7
y++*7
k = m = n
k=m=n
`.trim()} height={'270px'} initialTab={'verify'} />

## Produce

The EBNF producer generates words that follow the defined rules. Words are sorted by length and then lexicographically. Words are produced on the UI thread, so performance may vary with complex rules. In the future, I may move this to web workers for better performance.

You can experiment with the producer here:

<EbnfBlogWrapper initialRules={'<hello> <= "Hi, "\n<world> <= 世界\n<ebnf> <= [<hello> <world> {! | ?}]'} initialContent={''} height={'80px'} initialTab={'produce'} />

Keep in mind that depending on your EBNF ruleset, the number of possible words may grow exponentially as a function of word length.

## Compare

In the compare tab, you can compare two EBNF grammars for equality. After having two valid EBNF grammars on both the left and the right side, you can check for counterexamples with increasing word length.

<EbnfBlogWrapper initialRules={`
<left> <= [hello] {world?}
`.trim()} initialComparison={`
<right> <= hello {world}
`.trim()} height={'250px'} initialTab={'compare'} />

Again, the number of produced words can grow exponentially.

## EBNF language support

Language support extends beyond syntax errors and also encompasses some semantic errors, such as referencing a non-existing rule, as illustrated in the example below:

<EbnfBlogWrapper initialRules={`
<invalid> <= [no brackets
<rule> <= <rule_does_not_exist>
`.trim()} initialContent={''} height={'60px'} initialTab={'produce'} />

All errors have squiggly lines with a description upon hovering over the offending token.

The EBNF verifier/producer view below the rule editor automatically update once the ruleset changes, i.e. the verifier reevaluates whether the input matches the EBNF rule and the producer resets itself.

The producer also detects whether a given ruleset can only produce the empty word. There is also a check in place to detect whether no more words can be produced from the given EBNF ruleset.

<EbnfBlogWrapper initialRules={'<hello> <= ""\n<world> <= ""\n<ebnf> <= [<hello> <world>]'} initialContent={''} height={'80px'} initialTab={'produce'} />

## Next steps

You can also find the EBNF parser [here](/teaching/ebnf) outside the blog-post-context (or [here](/ebnf) for fullpage). There are still some things the editor could be extended with. This includes:

- Debounce input for rules, especially for larger rules
- Don't load monaco from an external CDN and use the webpack plugin
- Produce words in a web worker instead of doing it on the UI thread
  - Maybe don't produce words incrementally by word length but rather by some other useful incremental unit?
  - Also show produced words with virtual scroll
- Autocomplete using monaco's auto-complete API
- Add an escape character to e.g. allow matching quotation marks (`"`)
- serve as a PWA

**I do not guarantee the correctness of any results.** In case, you spot any errors, feel free to send me an [email](mailto:tgassmann@student.ethz.ch).

## Updates

<DetailsContainer>
<Details title="Update 2023-09-16">
You can now also use the above EBNF component as a web component:

```html
<ebnf-editor height="100px"></ebnf-editor>
<script type="module" src="https://thomasgassmann.com/widgets/ebnf.js"></script>
```

The `height` property is the only property that is currently exposed. It is required. The editor is going to take up the full width of its parent element.

**The web component is no longer published.** Use the [full page editor](/ebnf) instead.
</Details>

<Details title="Update 2023-09-20">

- Fixed some issues with the parser mistakenly accepting incomplete choice selections.
- Disallow creating empty rules (matched the empty string before)

</Details>

<Details title="Update 2023-09-22">

- Added fullscreen mode
- Moved share button to toolbar
- Show credits for parsely and docs in toolbar in all cases (not just when referenced via widget)
- Added [fullscreen page](/ebnf)

</Details>

<Details title="Update 2023-09-25">

- Added a neat easter egg for late-night EBNF enjoyers

</Details>

<Details title="Update 2023-09-27">

- Added full page mode support to EBNF widget. Use the fill property (the web component is no longer published, use the [full page editor](/ebnf) instead):
  ```html
  <ebnf-editor height="100px" fill="true"></ebnf-editor>
  <script type="module" src="https://thomasgassmann.com/widgets/ebnf.js"></script>
  ```
- Fixed an issue with CRLF / LF line breaks
- Added `Debug` button to print output of parser to console
- Clarify binding preference in documentation above (sequences bind stronger than selections)

</Details>

<Details title="Update 2023-09-30">

- Properly documented how to match empty sequences and emphasized that `ε` is not a keyword to do so within this editor

</Details>

<Details title="Update 2023-10-01">

- Do not show Debug button by default. Allow users to optionally enable it on the [debug page](/debug).

</Details>

<Details title="Update 2024-09-02">

- Add dark mode
- Update design to fit overall new website design.

</Details>

<Details title="Update 2024-09-24">

- Add feature to compare two EBNF grammars for equivalence

An example down below:

<EbnfBlogWrapper initialRules={`
<left> <= test{?}
`.trim()} initialComparison={`
<right> <= {test}
`.trim()} height={'250px'} initialTab={'compare'} />

</Details>

<Details title="Update 2025-10-08">

- Also support `<-` instead of `<=` for rule definitions (the course now uses `<-`)

</Details>

<Details title="Update 2026-09-30">

- Extracted EBNF Lab as a library at [github.com/thomasgassmann/ebnf-lab](https://github.com/thomasgassmann/ebnf-lab).
- This also includes a standalone site, so it can be hosted statically.

</Details>
</DetailsContainer>


Hi, I'm Thomas