We propose a separation logic-based approach for modular specification and verification of the I/O behavior of a program. The approach uses higher-order separation logic predicates to express abstract nested Hoare triples that abstractly associate a precondition and a postcondition with an I/O action. The approach supports verifying higher-level I/O actions built on top of lower-level ones (e.g. the I/O abstractions offered by the programming language’s standard library, implemented on top of system calls), as well as virtual I/O actions that in fact only manipulate memory, against specifications that are indistinguishable from those of the “primitive I/O actions”.