Disallow leading zeros in the prefix

cedar-policy · Oct 27, 2023 · cf7243d · cf7243d
1 parent 5ef3bf2
commit cf7243d
Show file tree

Hide file tree

Showing 2 changed files with 8 additions and 4 deletions.
diff --git a/cedar-dafny/def/ext/ipaddr.dfy b/cedar-dafny/def/ext/ipaddr.dfy
@@ -288,8 +288,8 @@ module def.ext.ipaddr.parseIPAddr {
         if 0 < |ds| <= 2
         then
           var n := DecStrToNat(ds);
-          if n <= V4_SIZE then
-            Some((n, ns'))
+          if n <= V4_SIZE && (ds[0] == '0' ==> (|ds| == 1 && n == 0)) then
+              Some((n, ns'))
           else None
         else None
       case None => None
@@ -530,7 +530,8 @@ module def.ext.ipaddr.parseIPAddr {
       case Some((ds, ns')) =>
         if 0 < |ds| <= 3 then
           var n := DecStrToNat(ds);
-          if n <= V6_SIZE then Some((n, ns'))
+          if n <= V6_SIZE && (ds[0] == '0' ==> (|ds| == 1 && n == 0)) then
+            Some((n, ns'))
           else None
         else None
       case None => None

diff --git a/cedar-dafny/test/ipaddr.dfy b/cedar-dafny/test/ipaddr.dfy
@@ -42,7 +42,10 @@ module test.ipaddr {
         "::::", // too many double colons
         "F:AE::F:5:F:F:0:0", // too many groups
         "F:A:F:5:F:F:0:0:1", // too many groups
-        "F:A" // too few groups
+        "F:A", // too few groups
+        "::/01", // leading zeros
+        "::/001", // leading zeros
+        "127.0.0.1/01" // leading zeros
       ];
     var i := |invalidStr| - 1;
     while 0 <= i {