initial commit
This commit is contained in:
134
doc/proposal.md
Normal file
134
doc/proposal.md
Normal file
@@ -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
|
||||||
|
|
||||||
Reference in New Issue
Block a user