grammar doc updates

2026-05-03 17:45:40 -07:00
parent 23ce29aece
commit 30427521ca
2 changed files with 283 additions and 582 deletions
--- a/doc/initial_proposal.md
+++ b/doc/initial_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 → <ThreatFeed, Log> 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<{}> -> <FlowMatch, Log> 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
+