Smart contracts, functioning autonomously within blockchain ecosystems, obviate the necessity for central oversight. Typically programmed in Solidity, these contracts interact with others on Ethereum via external calls that allow a contract to invoke a function of another contract. However, external calls lack mechanisms to ensure that the called code satisfies some predefined behavioral policies. In this paper, we propose a formal framework to specify and enforce security policies to address this issue. Specifically, we present a core calculus for smart contracts equipped with constructs for specifying policies at the code level, allowing for monitoring and enforcing desired behaviors. We provide the formal semantics of this calculus and describe how our approach can be used to detect and prevent flash loan-based arbitrage scenarios.