From 36a7af8065d7e789b1707a62254fb640c6e3ebdc Mon Sep 17 00:00:00 2001 From: Yuri Tatishchev Date: Fri, 1 May 2026 13:50:05 -0700 Subject: [PATCH] initial commit --- doc/proposal.md | 134 ++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 134 insertions(+) create mode 100644 doc/proposal.md diff --git a/doc/proposal.md b/doc/proposal.md new file mode 100644 index 0000000..925f160 --- /dev/null +++ b/doc/proposal.md @@ -0,0 +1,134 @@ + +## Idea + +Programming project: Firewall Language (FWL) - a higher level language for configuring firewall rules. + +Configuring firewalls with languages like nftables offers very limited static safety checks. + +The idea is to address these issues in FWL by treating firewall policy as a typed, functional program. Effectively this is a FWL is a DSL with two core features (planned, although I might have to change the scope a bit after I figure out more details) + +- a **refinement type system** that statically verifies exhaustiveness and non-overlap of network patterns at every layer +- an **algebraic effect system** that makes rule dependencies such as DNS lookups, threat feeds, connection state, etc. explicit in types, swappable between production and test, kind of analogous to typed dependency injection + +## Language Details + +For the initial version of the language, FWL would compile/transpile to nftables rules json. + +- Rules are typed functions over a layered `Frame` type that decomposes into protocol headers via pattern matching + - `Ether(eth, IPv4(ip, UDP(udp, payload)))` binds each header as a typed record; byte offsets are layer-relative and never written manually + - `pattern WGInitiation : (UDPHeader, Bytes<{}>) = (udp { length = 156 }, [0x01 _*])` +- Effects track side-effectful capabilities + - `rule r : Packet → Action` declares exactly what capabilities a rule needs; unhandled effects are type errors; handlers are swappable (production vs. mock) +- Sequence patterns express multi-packet protocol detection + - Some protocols (e.g. WireGuard) are only detectable over a multi-packet flow (3 packet handshake in this case) + - `WGInitiation . WGResponse within 5s` compiles to kernel `ct mark` state machines to offer a nicer syntax +- Exhaustiveness checking, static interface declaration + - CIDR arms must tile their parent prefix; port arms must tile their parent range; ADT arms must cover all constructors + - `interface lan cidr4 = {10.17.1.0/24}` makes CIDR membership a compile-time-resolved refinement + +## Example + +Example firewall setup for a home router, syntax details subject to change + +``` +-- interfaces +interface wan : WAN dynamic +interface lan : LAN cidr4 = { 10.17.1.0/24 } + cidr6 = { fe80::/10, fd12:3456::/48 } +interface wg0 : WireGuard + +zone lan_zone = { lan, wg0 } + +import rfc1918 : CIDRSet from "builtin:rfc1918" + +-- port forwarding table +let forwards : Map<(Protocol, Port), (IP, Port)> = { + (tcp, :8080) -> (10.17.1.10, :80), + (tcp, :2222) -> (10.17.1.11, :22) +} + +-- WireGuard handshake detection (compiles to kernel ct mark — no NFQUEUE) +pattern WGInitiation : (UDPHeader, Bytes<{}>) = (udp { length = 156 }, [0x01 _*]) +pattern WGResponse : (UDPHeader, Bytes<{}>) = (udp { length = 100 }, [0x02 _*]) + +flow WireGuardHandshake : FlowPattern = WGInitiation . WGResponse within 5s + +-- block LAN clients from tunnelling out via WireGuard +rule blockOutboundWG : Frame<{}> -> Action = + \frame -> case frame of + | Frame(iif ∈ lan_zone -> wan, + Ether(_, IPv4(ip { src ∈ lan.cidr4 }, WGInitiation))) -> + case perform FlowMatch.check(flowOf(ip, wg), WireGuardHandshake) of + | Matched -> Log.emit(Warn, "WG blocked: " ++ show ip.src) >> Drop + | _ -> Continue + | _ -> Continue + +-- NAT +policy nat_prerouting : Frame<{}> + on hook = Prerouting, table = NAT, priority = DstNat + where + | Frame(_, Ether(_, IPv4(ip, _))) -> + perform FIB.daddrLocal(ip.dst) >>= \local -> + if local then DNATMap(forwards) else Allow + | _ -> Allow + +policy nat_postrouting : Frame<{}> + on hook = Postrouting, table = NAT, priority = SrcNat + where + | Frame(_ -> wan, Ether(_, IPv4(ip { src ∈ rfc1918 }, _))) -> Masquerade + | _ -> Allow + +-- inbound (to router) +policy input : Frame<{}> + on hook = Input, table = Filter, priority = Filter + where + | _ if ct.state ∈ {Established, Related} -> Allow + | Frame(lo, _) -> Allow + | Frame(_, Ether(_, IPv6(ip6 { src ∈ fe80::/10 }, ICMPv6(_, _)))) -> Allow + | Frame(_, Ether(_, IPv4(_, TCP(tcp { dport = :22 }, _)))) -> Allow + | Frame(_, Ether(_, IPv4(_, UDP(udp { dport = :51944 }, _)))) -> Allow + | _ -> Drop + +-- forwarded traffic +policy forward : Frame<{}> + on hook = Forward, table = Filter, priority = Filter + where + | _ if ct.state ∈ {Established, Related} -> Allow + | frame if iif ∈ lan_zone && oif == wan -> blockOutboundWG(frame) + | _ if ct.status == DNAT -> Allow + | Frame(iif ∈ lan_zone -> wan, _) -> Allow + | Frame(iif ∈ lan_zone -> lan_zone, _) -> Allow + | Frame(wan -> lan_zone, + Ether(_, IPv4(ip, TCP(tcp, _)))) + if (ip.dst, tcp.dport) ∈ forwards -> Allow + | _ -> Drop + +-- outbound (from router) +policy output : Frame<{}> + on hook = Output, table = Filter, priority = Filter + where + | _ -> Allow +``` + +## Weekly Plan + +1. Week 1: Design & Parser + 1. finalize AST design + 2. Parsec parser for all declarations + 3. pretty printer +2. Week 2: Type Checker + 1. effect row inference + 2. label exhaustiveness + 3. CIDR/port interval checker +3. Week 3: Interpreter + 1. perform`/`handle` dispatch + 2. mock handler environment + 3. test suite +4. Week 4: Compiler/Transpiler + 1. generate nftables json + 2. convert sequence patterns to `ct mark` + 3. test with `nft -f` +5. Week 5: Presentation stuff + 1. make slides and all that + 2. practice presenting +