从 4.14.1 升级到 4.15.3 后,计算和内存均出现回退
(declare-fun p () String) (declare-fun an () String) (declare-fun pa () String) (declare-fun r () String) (declare-fun a () String) (assert (= p "arn:AWS:iam::012345678901:role/RoleInQuestion")) (assert (let ((a!1 (re.++ (re.++ (str.to_re "arn:AWS:s3:::") (re.* (re.range "!" "")))
(str.to_re "cloudtrail")))
(a!2 (re.++ (re.++ (str.to_re "arn:AWS:s3:::") (re.* (re.range "!" "")))
(str.to_re "controltower")))
(a!4 (and (or (= a "s3:listallmybuckets") (= a "s3:listbucket") (= a "s3:listmultiregionaccesspoints"))
(str.in_re r (re.* (re.range "!" "")))
(= pa "arn:AWS:iam::AWS:policy/job-function/ViewOnlyAccess")))
(a!5 (and (or (= a "s3:listaccessgrants") (= a "s3:listaccessgrantsinstances") (= a "s3:listaccesspoints") (= a "s3:listaccesspointsforobjectlambda") (= a "s3:listallmybuckets") (= a "s3:listbucket") (= a "s3:listcalleraccessgrants") (= a "s3:listjobs") (= a "s3:listmultiregionaccesspoints") (= a "s3:liststoragelensconfigurations") (= a "s3:liststoragelensgroups") (= a "s3:describejob") (= a "s3:getaccelerateconfiguration") (= a "s3:getaccessgrantsinstanceresourcepolicy") (= a "s3:getaccesspoint") (= a "s3:getaccesspointconfigurationforobjectlambda") (= a "s3:getaccesspointforobjectlambda") (= a "s3:getaccesspointpolicy") (= a "s3:getaccesspointpolicyforobjectlambda") (= a "s3:getaccesspointpolicystatus") (= a "s3:getaccesspointpolicystatusforobjectlambda") (= a "s3:getaccountpublicaccessblock") (= a "s3:getanalyticsconfiguration") (= a "s3:getencryptionconfiguration") (= a "s3:getinventoryconfiguration") (= a "s3:getlifecycleconfiguration") (= a "s3:getmetricsconfiguration") (= a "s3:getmultiregionaccesspoint") (= a "s3:getmultiregionaccesspointpolicy") (= a "s3:getmultiregionaccesspointpolicystatus") (= a "s3:getobjectacl") (= a "s3:getobjecttagging") (= a "s3:getobjectversionacl") (= a "s3:getreplicationconfiguration") (= a "s3:getstoragelensconfiguration") (= a "s3:getstoragelensgroup") (str.prefixof "s3:getbucket" a))
(str.in_re r (re.* (re.range "!" "")))
(= pa "arn:AWS:iam::AWS:policy/SecurityAudit")))
(a!6 (and (= a "s3:getobject")
…
内容来源: Z3Prover/z3