## 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