Theory Parser
section‹Parser for iptables-save›
theory Parser
imports Code_Interface
keywords "parse_iptables_save" :: thy_decl
begin
ML‹
fun takeWhile p xs = take_prefix p xs;
fun dropWhile p xs = drop_prefix p xs;
fun dropWhileInclusive p xs = drop 1 (dropWhile p xs)
fun split_at p xs = (takeWhile p xs, dropWhileInclusive p xs);
›
ML_val‹
split_at (fn x => x <> " ") (raw_explode "foo bar")
›
section‹An SML Parser for iptables-save›
text‹Work in Progress›
ML‹
local
fun is_start_of_table table s = s = ("*"^table);
fun is_end_of_table s = s = "COMMIT";
fun load_file (thy: theory) (path: string list) =
let val p = File.full_path (Resources.master_directory thy) (Path.make path);
val _ = "loading file "^File.platform_path p |> writeln;
in
if
not (File.exists p) orelse (File.is_dir p)
then
raise Fail "File not found"
else
File.read_lines p
end;
fun extract_table _ [] = []
| extract_table table (r::rs) = if not (is_start_of_table table r)
then
extract_table table rs
else
takeWhile (fn x => not (is_end_of_table x)) rs;
fun writenumloaded table_name table = let
val _ = "Loaded "^ Int.toString (length table) ^" lines of the "^table_name^" table" |> writeln;
in table end;
fun warn_windows_line_endings lines =
let
val warn = fn s => if String.isSuffix "\r" s
then
writeln "WARNING: windows \\r\\n line ending detected"
else
()
val _ = map warn lines
in
lines
end;
in
fun load_table table thy = load_file thy
#> warn_windows_line_endings
#> extract_table table
#> writenumloaded table;
val load_filter_table = load_table "filter";
end;
›
ML‹
local
fun collapse_quotes [] = []
| collapse_quotes ("\""::ss) = let val (quoted, rest) = split_at (fn x => x <> "\"") ss in
"\"" ^ implode quoted^"\"" :: rest end
| collapse_quotes (s::ss) = s :: collapse_quotes ss;
in
val ipt_explode = raw_explode #> collapse_quotes;
end
›
ML_val‹
ipt_explode "ad \"as das\" boo";
ipt_explode "ad \"foobar --boo boo";
ipt_explode "ent \"\\\"\" this";
ipt_explode "";
›
ML‹
datatype parsed_action_type = TypeCall | TypeGoto
datatype parsed_match_action = ParsedMatch of term
| ParsedNegatedMatch of term
| ParsedAction of parsed_action_type * string;
local
val is_whitespace = Scan.many (fn x => x = " ");
local
local
fun extract_int ss = case ss |> implode |> Int.fromString
of SOME i => i
| NONE => raise Fail "unparsable int";
fun is_iface_char x = Symbol.is_ascii x andalso
(Symbol.is_ascii_letter x orelse Symbol.is_ascii_digit x orelse x = "+"
orelse x = "*" orelse x = "." orelse x = "-")
in
fun mk_nat maxval i = if i < 0 orelse i > maxval
then
raise Fail("nat ("^Int.toString i^") must be between 0 and "^Int.toString maxval)
else (HOLogic.mk_number HOLogic.natT i);
fun ipNetmask_to_hol (ip,len) = @{const IpAddrNetmask (32)} $ mk_ipv4addr ip $ mk_nat 32 len;
fun ipRange_to_hol (ip1,ip2) = @{const IpAddrRange (32)} $ mk_ipv4addr ip1 $ mk_ipv4addr ip2;
val parser_ip_cidr = parser_ipv4 --| ($$ "/") -- (Scan.many1 Symbol.is_ascii_digit >> extract_int) >> ipNetmask_to_hol;
val parser_ip_range = parser_ipv4 --| ($$ "-") -- parser_ipv4 >> ipRange_to_hol;
val parser_ip_addr = parser_ipv4 >> (fn ip => @{const IpAddr (32)} $ mk_ipv4addr ip);
val parser_interface = Scan.many1 is_iface_char >> (implode #> (fn x => @{const Iface} $ HOLogic.mk_string x));
val parser_protocol = Scan.this_string "tcp" >> K @{term "TCP :: 8 word"}
|| Scan.this_string "udp" >> K @{term "UDP :: 8 word"}
|| (Scan.this_string "icmpv6" || Scan.this_string "ipv6-icmp")
>> K @{term "L4_Protocol.IPv6ICMP"}
|| Scan.this_string "icmp" >> K @{term "ICMP :: 8 word"}
|| Scan.this_string "esp" >> K @{term "L4_Protocol.ESP"}
|| Scan.this_string "ah" >> K @{term "L4_Protocol.AH"}
|| Scan.this_string "gre" >> K @{term "L4_Protocol.GRE"}
val parser_ctstate = Scan.this_string "NEW" >> K @{const CT_New}
|| Scan.this_string "ESTABLISHED" >> K @{const CT_Established}
|| Scan.this_string "RELATED" >> K @{const CT_Related}
|| Scan.this_string "UNTRACKED" >> K @{const CT_Untracked}
|| Scan.this_string "INVALID" >> K @{const CT_Invalid}
val parser_tcp_flag = Scan.this_string "SYN" >> K @{const TCP_SYN}
|| Scan.this_string "ACK" >> K @{const TCP_ACK}
|| Scan.this_string "FIN" >> K @{const TCP_FIN}
|| Scan.this_string "RST" >> K @{const TCP_RST}
|| Scan.this_string "URG" >> K @{const TCP_URG}
|| Scan.this_string "PSH" >> K @{const TCP_PSH}
fun parse_comma_separated_list parser = Scan.repeat (parser --| $$ ",") @@@ (parser >> (fn p => [p]))
local
val mk_port_single = mk_nat 65535 #> (fn n => @{const nat_to_16word} $ n)
val parse_port_raw = Scan.many1 Symbol.is_ascii_digit >> extract_int
fun port_tuple_warn (p1,p2) =
if p1 >= p2
then
let val _= writeln ("WARNING (in ports): "^Int.toString p1^" >= "^Int.toString p2)
in (p1, p2) end
else (p1, p2);
in
val parser_port_single_tup = (
(parse_port_raw --| $$ ":" -- parse_port_raw)
>> (port_tuple_warn #> (fn (p1,p2) => (mk_port_single p1, mk_port_single p2)))
|| (parse_port_raw >> (fn p => (mk_port_single p, mk_port_single p)))
) >> HOLogic.mk_prod
end
val parser_port_single_tup_term = parser_port_single_tup
>> (fn x => @{term "L4Ports 0"} $ HOLogic.mk_list @{typ "16 word × 16 word"} [x])
val parser_port_many1_tup = parse_comma_separated_list parser_port_single_tup
>> (fn x => @{term "L4Ports 0"} $ HOLogic.mk_list @{typ "16 word × 16 word"} x)
val parser_ctstate_set = parse_comma_separated_list parser_ctstate
>> HOLogic.mk_set @{typ "ctstate"}
val parser_tcp_flag_set = parse_comma_separated_list parser_tcp_flag
>> HOLogic.mk_set @{typ "tcp_flag"}
val parser_tcp_flags = (parser_tcp_flag_set --| $$ " " -- parser_tcp_flag_set)
>> (fn (m,c) => @{const TCP_Flags} $ m $ c)
val parser_extra = Scan.many1 (fn x => x <> " " andalso Symbol.not_eof x)
>> (implode #> HOLogic.mk_string);
end;
val eoo = Scan.ahead ($$ " " || Scan.one Symbol.is_eof);
fun parse_cmd_option_generic (d: term -> parsed_match_action) s t (parser: string list -> (term * string list)) =
Scan.finite Symbol.stopper (is_whitespace |-- Scan.this_string s |-- (parser >> (fn r => d (t $ r))) --| eoo)
fun parse_cmd_option (s: string) (t: term) (parser: string list -> (term * string list)) =
parse_cmd_option_generic ParsedMatch s t parser;
fun parse_cmd_option_negated (s: string) (t: term) (parser: string list -> (term * string list)) =
parse_cmd_option_generic ParsedNegatedMatch ("! "^s) t parser || parse_cmd_option s t parser;
fun parse_cmd_option_negated_singleton s t parser = parse_cmd_option_negated s t parser >> (fn x => [x])
fun parse_with_module_prefix (module: string) (parser: (string list -> parsed_match_action * string list)) =
(Scan.finite Symbol.stopper (is_whitespace |-- Scan.this_string module)) |-- (Scan.repeat parser)
in
val parse_ips = parse_cmd_option_negated_singleton "-s " @{const Src (32)} (parser_ip_cidr || parser_ip_addr)
|| parse_cmd_option_negated_singleton "-d " @{const Dst (32)} (parser_ip_cidr || parser_ip_addr);
val parse_iprange = parse_with_module_prefix "-m iprange "
( parse_cmd_option_negated "--src-range " @{const Src (32)} parser_ip_range
|| parse_cmd_option_negated "--dst-range " @{const Dst (32)} parser_ip_range);
val parse_iface = parse_cmd_option_negated_singleton "-i " @{const IIface (32)} parser_interface
|| parse_cmd_option_negated_singleton "-o " @{const OIface (32)} parser_interface;
val parse_protocol = parse_cmd_option_negated_singleton "-p "
@{term "(Prot ∘ Proto) :: primitive_protocol ⇒ 32 common_primitive"} parser_protocol;
val parse_tcp_options = parse_with_module_prefix "-m tcp "
( parse_cmd_option_negated "--sport " @{const Src_Ports (32)} parser_port_single_tup_term
|| parse_cmd_option_negated "--dport " @{const Dst_Ports (32)} parser_port_single_tup_term
|| parse_cmd_option_negated "--tcp-flags " @{const L4_Flags (32)} parser_tcp_flags);
val parse_multiports = parse_with_module_prefix "-m multiport "
( parse_cmd_option_negated "--sports " @{const Src_Ports (32)} parser_port_many1_tup
|| parse_cmd_option_negated "--dports " @{const Dst_Ports (32)} parser_port_many1_tup
|| parse_cmd_option_negated "--ports " @{const MultiportPorts (32)} parser_port_many1_tup);
val parse_udp_options = parse_with_module_prefix "-m udp "
( parse_cmd_option_negated "--sport " @{const Src_Ports (32)} parser_port_single_tup_term
|| parse_cmd_option_negated "--dport " @{const Dst_Ports (32)} parser_port_single_tup_term);
val parse_ctstate = parse_with_module_prefix "-m state "
(parse_cmd_option_negated "--state " @{const CT_State (32)} parser_ctstate_set)
|| parse_with_module_prefix "-m conntrack "
(parse_cmd_option_negated "--ctstate " @{const CT_State (32)} parser_ctstate_set);
val parse_unknown = (parse_cmd_option "" @{const Extra (32)} parser_extra) >> (fn x => [x]);
end;
local
fun is_target_char x = Symbol.is_ascii x andalso
(Symbol.is_ascii_letter x orelse Symbol.is_ascii_digit x orelse x = "-" orelse x = "_" orelse x = "~")
fun parse_finite_skipwhite parser = Scan.finite Symbol.stopper (is_whitespace |-- parser);
val is_icmp_type = fn x => Symbol.is_ascii_letter x orelse x = "-" orelse x = "6"
in
val parser_target = Scan.many1 is_target_char >> implode;
val parse_target_generic : (string list -> parsed_match_action * string list) = parse_finite_skipwhite
(Scan.this_string "-j " |-- (parser_target >> (fn s => ParsedAction (TypeCall, s))));
val parse_target_reject : (string list -> parsed_match_action * string list) = parse_finite_skipwhite
(Scan.this_string "-j " |-- (Scan.this_string "REJECT" >> (fn s => ParsedAction (TypeCall, s)))
--| ((Scan.this_string " --reject-with " --| Scan.many1 is_icmp_type) || Scan.this_string ""));
val parse_target_goto : (string list -> parsed_match_action * string list) = parse_finite_skipwhite
(Scan.this_string "-g " |-- (parser_target >> (fn s => let val _ = writeln ("WARNING: goto in `"^s^"'") in ParsedAction (TypeGoto, s) end)));
val parse_target : (string list -> parsed_match_action * string list) = parse_target_reject || parse_target_goto || parse_target_generic;
end;
in
val parse_table_append : (string list -> (string * string list)) = Scan.this_string "-A " |-- parser_target --| is_whitespace;
val option_parser : (string list -> (parsed_match_action list) * string list) =
Scan.recover (parse_ips || parse_iprange
|| parse_iface
|| parse_protocol
|| parse_tcp_options || parse_udp_options || parse_multiports
|| parse_ctstate
|| parse_target >> (fn x => [x])) (K parse_unknown);
local
val custom_chain_decl_parser = ($$ ":") |-- parser_target --| Scan.this_string " - " #> fst;
val builtin_chain_decl_parser = ($$ ":") |--
(Scan.this_string "INPUT" || Scan.this_string "FORWARD" || Scan.this_string "OUTPUT" || Scan.this_string "PREROUTING") --|
($$ " ") -- (Scan.this_string "ACCEPT" || Scan.this_string "DROP") --| ($$ " ") #> fst;
val wrap_builtin_chain = (fn (name, policy) => (name, SOME policy));
val wrap_custom_chain = (fn name => (name, NONE));
in
val chain_decl_parser : (string list -> string * string option) =
Scan.recover (builtin_chain_decl_parser #> wrap_builtin_chain) (K (custom_chain_decl_parser #> wrap_custom_chain));
end
end;
›
ML‹
local
fun concat [] = []
| concat (x :: xs) = x @ concat xs;
in
fun Scan_cons_repeat (parser: ('a -> 'b list * 'a)) (s: 'a) : ('b list * 'a) =
let val (x, rest) = Scan.repeat parser s in (concat x, rest) end;
end
›
ML_val‹(Scan_cons_repeat option_parser) (ipt_explode "-i lup -j net-fw")›
ML_val‹(Scan_cons_repeat option_parser) (ipt_explode "")›
ML_val‹(Scan_cons_repeat option_parser) (ipt_explode "-i lup foo")›
ML_val‹(Scan_cons_repeat option_parser) (ipt_explode "-m tcp --dport 22 --sport 88")›
ML_val‹(Scan_cons_repeat option_parser) (ipt_explode "-j LOG --log-prefix \"Shorewall:INPUT:REJECT:\" --log-level 6")›
ML_val‹
val (x, rest) = (Scan_cons_repeat option_parser) (ipt_explode "-d 0.31.123.213/11. --foo_bar \"he he\" -f -i eth0+ -s 0.31.123.213/21 moreextra -j foobar --log");
map (fn p => case p of ParsedMatch t => type_of t | ParsedAction (_,_) => dummyT) x;
map (fn p => case p of ParsedMatch t => Pretty.writeln (Syntax.pretty_term @{context} t) | ParsedAction (_,a) => writeln ("action: "^a)) x;
›
ML‹
local
fun parse_rule_options (s: string list) : parsed_match_action list = let
val (parsed, rest) = (case try (Scan.catch (Scan_cons_repeat option_parser)) s
of SOME x => x
| NONE => raise Fail "scanning")
in
if rest <> []
then
raise Fail ("Unparsed: `"^implode rest^"'")
else
parsed
end
handle Fail m => raise Fail ("parse_rule_options: "^m^" for rule `"^implode s^"'");
fun get_target (ps : parsed_match_action list) : (parsed_action_type * string) option = let
val actions = List.mapPartial (fn p => case p of ParsedAction a => SOME a
| _ => NONE) ps
in case actions of [] => NONE
| [action] => SOME action
| _ => raise Fail "there can be at most one target"
end;
val get_matches : (parsed_match_action list -> term) =
List.mapPartial (fn p => case p of
ParsedMatch m => SOME (@{const Pos ("32 common_primitive")} $ m)
| ParsedNegatedMatch m => SOME (@{const Neg ("32 common_primitive")} $ m)
| ParsedAction _ => NONE)
#> HOLogic.mk_list @{typ "32 common_primitive negation_type"};
fun parse_rule (s: string) : (string * (parsed_action_type * string) option * term) = let
val (chainname, rest) =
(case try (ipt_explode #> Scan.finite Symbol.stopper parse_table_append) s
of SOME x => x
| NONE => raise Fail ("parse_rule: parse_table_append: "^s));
val parsed = parse_rule_options rest
in (chainname, get_target parsed, get_matches parsed) end;
in
fun rule_type_partition (rs : string list) : ((string * string option) list * (string * (parsed_action_type * string) option * term) list) =
let
val (chain_decl, rules) = List.partition (String.isPrefix ":") rs
in
if not (List.all (String.isPrefix "-A") rules)
then
raise Fail "could not partition rules"
else
let val parsed_chain_decls = (case try (map (ipt_explode #> chain_decl_parser)) chain_decl
of SOME x => x
| NONE => raise Fail ("could not parse chain declarations: "^implode chain_decl));
val parsed_rules = map parse_rule rules;
val _ = "Parsed "^ Int.toString (length parsed_chain_decls) ^" chain declarations" |> writeln;
val _ = "Parsed "^ Int.toString (length parsed_rules) ^" rules" |> writeln;
in (parsed_chain_decls, parsed_rules) end
end
fun get_chain_decls_policy (ls: ((string * string option) list * (string * (parsed_action_type * string) option * term) list)) = fst ls
fun get_parsed_rules (ls: ((string * string option) list * (string * (parsed_action_type * string) option * term) list)) = snd ls
val filter_chain_decls_names_only :
((string * string option) list * (string * (parsed_action_type * string) option * term) list) ->
(string list * (string * (parsed_action_type * string) option * term) list) = (fn (a,b) => (map fst a, b))
end;
›
ML‹
structure FirewallTable = Table(type key = string; val ord = Library.string_ord);
type firewall_table = term list FirewallTable.table;
local
fun FirewallTable_init chain_decls : firewall_table = FirewallTable.empty
|> fold (fn entry => fn accu => FirewallTable.update_new (entry, []) accu) chain_decls;
fun hacky_hack t =
@{const alist_and' ("32 common_primitive")} $ (@{const fill_l4_protocol (32)} $ (@{const compress_parsed_extra (32)} $ t))
fun mk_MatchExpr t = if fastype_of t <> @{typ "32 common_primitive negation_type list"}
then
raise Fail "Type Error"
else
hacky_hack t;
fun mk_Rule_help t a = let val r = @{const Rule ("32 common_primitive")} $ (mk_MatchExpr t) $ a in
if fastype_of r <> @{typ "32 common_primitive rule"} then raise Fail "Type error in mk_Rule_help"
else r end;
fun append table chain rule = case FirewallTable.lookup table chain
of NONE => raise Fail ("uninitialized cahin: "^chain)
| SOME rules => FirewallTable.update (chain, rules@[rule]) table
fun mk_Rule (tbl: firewall_table) (chain: string, target : (parsed_action_type * string) option, t : term) =
if not (FirewallTable.defined tbl chain)
then
raise Fail ("undefined chain to be appended: "^chain)
else case target
of NONE => mk_Rule_help t @{const action.Empty}
| SOME (TypeCall, "ACCEPT") => mk_Rule_help t @{const action.Accept}
| SOME (TypeCall, "DROP") => mk_Rule_help t @{const action.Drop}
| SOME (TypeCall, "REJECT") => mk_Rule_help t @{const action.Reject}
| SOME (TypeCall, "LOG") => mk_Rule_help t @{const action.Log}
| SOME (TypeCall, "RETURN") => mk_Rule_help t @{const action.Return}
| SOME (TypeCall, custom) => if not (FirewallTable.defined tbl custom)
then
raise Fail ("unknown action: "^custom)
else
mk_Rule_help t (@{const action.Call} $ HOLogic.mk_string custom)
| SOME (TypeGoto, "ACCEPT") => raise Fail "Unexpected"
| SOME (TypeGoto, "DROP") => raise Fail "Unexpected"
| SOME (TypeGoto, "REJECT") => raise Fail "Unexpected"
| SOME (TypeGoto, "LOG") => raise Fail "Unexpected"
| SOME (TypeGoto, "RETURN") => raise Fail "Unexpected"
| SOME (TypeGoto, custom) => if not (FirewallTable.defined tbl custom)
then
raise Fail ("unknown action: "^custom)
else
mk_Rule_help t (@{const action.Goto} $ HOLogic.mk_string custom);
in
local
fun append_rule (tbl: firewall_table) (chain: string, target : (parsed_action_type * string) option, t : term) = append tbl chain (mk_Rule tbl (chain, target, t))
in
fun make_firewall_table (parsed_chain_decls : string list, parsed_rules : (string * (parsed_action_type * string) option * term) list) =
fold (fn rule => fn accu => append_rule accu rule) parsed_rules (FirewallTable_init parsed_chain_decls);
end
end
›
ML‹
fun mk_Ruleset (tbl: firewall_table) = FirewallTable.dest tbl
|> map (fn (k,v) => HOLogic.mk_prod (HOLogic.mk_string k, HOLogic.mk_list @{typ "32 common_primitive rule"} v))
|> HOLogic.mk_list @{typ "string × 32 common_primitive rule list"}
›
ML‹
local
fun default_policy_action_to_term "ACCEPT" = @{const "action.Accept"}
| default_policy_action_to_term "DROP" = @{const "action.Drop"}
| default_policy_action_to_term a = raise Fail ("Not a valid default policy `"^a^"'")
in
fun preparedefault_policies [] = []
| preparedefault_policies ((chain_name, SOME default_policy)::ls) =
(chain_name, default_policy_action_to_term default_policy) :: preparedefault_policies ls
| preparedefault_policies ((_, NONE)::ls) = preparedefault_policies ls
end
›
ML‹
fun trace_timing (printstr : string) (f : 'a -> 'b) (a : 'a) : 'b =
let val t0 = Time.now(); in
let val result = f a; in
let val t1= Time.now(); in
let val _ = writeln(String.concat [printstr^" (", Time.toString(Time.-(t1,t0)), " seconds)"]) in
result
end end end end;
fun simplify_code ctxt = let val _ = writeln "unfolding (this may take a while) ..." in
trace_timing "Simplified term" (Code_Evaluation.dynamic_value_strict ctxt)
end
fun certify_term ctxt t = trace_timing "Certified term" (Thm.cterm_of ctxt) t
›
ML_val‹
fun parse_iptables_save_global thy (file: string list) : term =
load_filter_table thy file
|> rule_type_partition
|> filter_chain_decls_names_only
|> make_firewall_table
|> mk_Ruleset
|> simplify_code @{context}
›
ML‹
local
fun define_const t name lthy = let
val binding_name = Thm.def_binding name
val _ = writeln ("Defining constant `" ^ Binding.name_of binding_name ^ "'");
in
lthy
|> Proof_Context.set_stmt false
|> Local_Theory.define ((name, NoSyn), ((binding_name, @{attributes [code]}), t)) |> #2
end;
fun print_default_policies (ps: (string * term) list) = let
val _ = ps |> map (fn (name, _) =>
if name <> "INPUT" andalso name <> "FORWARD" andalso name <> "OUTPUT"
then
writeln ("WARNING: the chain `"^name^"' is not a built-in chain of the filter table")
else ())
in ps end;
fun sanity_check_ruleset ctxt t = let
val check = Code_Evaluation.dynamic_value_strict ctxt (@{const sanity_wf_ruleset ("32 common_primitive")} $ t)
in
if check <> @{term "True"} then raise ERROR "sanity_wf_ruleset failed" else t
end;
in
fun parse_iptables_save table name path lthy =
let
val prepared = path
|> load_table table (Proof_Context.theory_of lthy)
|> rule_type_partition
val firewall = prepared
|> filter_chain_decls_names_only
|> make_firewall_table
|> mk_Ruleset
|> simplify_code lthy
|> trace_timing "checked sanity with sanity_wf_ruleset" (sanity_check_ruleset lthy)
val default_policis = prepared
|> get_chain_decls_policy
|> preparedefault_policies
|> print_default_policies
in
lthy
|> define_const firewall name
|> fold (fn (chain_name, policy) =>
define_const policy (Binding.name (Binding.name_of name ^ "_" ^ chain_name ^ "_default_policy")))
default_policis
end
end
›
ML‹
Outer_Syntax.local_theory @{command_keyword parse_iptables_save}
"load a file generated by iptables-save and make the firewall definition available as isabelle term"
(Parse.binding --| @{keyword "="} -- Scan.repeat1 Parse.path >>
(fn (binding, paths) => parse_iptables_save "filter" binding paths))
›
end