no zero address msg sender in exposure opening on new rollover certora

term-finance · Jun 21, 2024 · 42a611e · 42a611e
1 parent 4621474
commit 42a611e
Showing 1 changed file with 2 additions and 1 deletion.
diff --git a/certora/specs/termRepoServicer/rolloverExposure.spec b/certora/specs/termRepoServicer/rolloverExposure.spec
@@ -56,7 +56,8 @@ rule openExposureOnRolloverNewIntegrity(env e) {
     require(rolloverExposureController.getTreasuryAddress() != e.msg.sender); // Protecting treasury from calling this function
     require(rolloverExposureController.getTreasuryAddress() != rolloverExposureLocker); // Protecting locker from using treasury address;
     require(rolloverExposureController.getTreasuryAddress() != previousTermRepoLocker); // Protecting previous locker from using treasury address;
-
+    require(e.msg.sender != 0); // Protecting from zero address
+
     mathint balanceBefore = getBorrowerRepurchaseObligation(borrower);
     mathint tokenBalanceTermRepoLockerBefore = rolloverExposureToken.balanceOf(rolloverExposureLocker);
     mathint tokenBalancePreviousTermRepoLockerBefore = rolloverExposureToken.balanceOf(previousTermRepoLocker);