Disallow leading zeros in the IP address prefix. (#140)

Co-authored-by: Emina Torlak <[email protected]>
cedar-policy · Oct 30, 2023 · 0b0ccea · 0b0ccea
1 parent 4072beb
commit 0b0ccea
Show file tree

Hide file tree

Showing 2 changed files with 8 additions and 3 deletions.
diff --git a/cedar-lean/Cedar/Spec/Ext/IPAddr.lean b/cedar-lean/Cedar/Spec/Ext/IPAddr.lean
@@ -148,7 +148,7 @@ def IPNet.isMulticast (ip : IPNet) : Bool :=
 
 def parseCIDR (str : String) (digits : Nat) (size : Nat) : Option (Fin (size + 1)) :=
   let len := str.length
-  if 0 < len && len ≤ digits
+  if 0 < len && len ≤ digits && (str.startsWith "0" → str = "0")
   then do
     let n ← str.toNat?
     if n ≤ size then .some (Fin.ofNat n) else .none

diff --git a/cedar-lean/UnitTest/IPAddr.lean b/cedar-lean/UnitTest/IPAddr.lean
@@ -64,7 +64,12 @@ def testsForInvalidStrings :=
     testInvalid "F:A" "too few groups",
     testInvalid "::ffff1" "group out of range",
     testInvalid "F:AE::F:5:F:F:0/129" "prefix out of range",
-    testInvalid "::ffff:127.0.0.1" "no IPv4 embedded in IPv6"
+    testInvalid "::ffff:127.0.0.1" "no IPv4 embedded in IPv6",
+    testInvalid "::/00" "no leading zeros",
+    testInvalid "::/01" "no leading zeros",
+    testInvalid "::/001" "no leading zeros",
+    testInvalid "127.0.0.1/01" "no leading zeros",
+    testInvalid "F:AE::F:5:F:F:0/01" "no leading zeros"
   ]
 
 deriving instance Inhabited for IPNet
@@ -163,4 +168,4 @@ def tests := [
 -- Uncomment for interactive debugging
 -- #eval TestSuite.runAll tests
 
-end UnitTest.IPAddr
+end UnitTest.IPAddr