Virtually all computer programs are written in high-level languages. A suitable source language can impose certain desirable properties (like memory or type safety), or it can facilitate reasoning about a program satisfying a given spec (formally or informally). However, there is a deep gulf between programs as they are written and executed: compiled to low-level representations, and running in an untrusted medium where source-level guarantees dissolve. And whereas the correctness of compilation is a well-understood problem with proven solutions, its security considerations are much less clear. In particular, what security guarantees should a compiler provide, and how can we specify them formally? Can we implement them efficiently and verify them with reasonable effort? And can we hope to achieve all this for practical programming languages, compilers and hardware? In this talk I will present our answers to these questions through SECOMP, a fully verified secure compiler that builds security on top of the CompCert C verified compiler. These include a flexible compartment model for CompCert C, security definitions and scalable proof techniques for them, and low-level enforcement based on CHERI-style capability machines.