The recent Spectre attacks exploit speculative execution and microarchitectural side channels, such as caches, to leak sensitive information. Since the underlying hardware vulnerabilities are here to stay in billions of deployed devices, software countermeasures have been developed. Rigorously reasoning about their effectiveness, however, requires a well-defined notion of security against speculative execution attacks, which has been missing until now. We put forward speculative non-interference, the first semantic notion of security against speculative execution attacks, and we develop Spectector, an algorithm based on symbolic execution to automatically prove speculative non-interference, or to detect violations. We implement Spectector in a tool, which we use to detect subtle leaks and optimizations opportunities in the way major compilers place Spectre countermeasures.