Software protections against side-channel and physical attacks are
essential to the development of secure applications. Such
protections are meaningful at machine code or micro-architectural
level, but they typically do not carry observable semantics at
source level. This renders them susceptible to miscompilation, and
security engineers embed input/output side-effects to prevent
optimizing compilers from altering them. Yet these side-effects are
error-prone and compiler-dependent. The current practice involves
analyzing the generated machine code to make sure security or
privacy properties are still enforced. These side-effects may also
be too expensive in fine-grained protections such as control-flow
integrity. We introduce observations of the program state that are
intrinsic to the correct execution of security protections, along
with means to specify and preserve observations across the
compilation flow. Such observations complement the input/output
semantics-preservation contract of compilers. We introduce an
opacification mechanism to preserve and enforce a partial ordering
of observations. This approach is compatible with a production
compiler and does not incur any modification to its optimization
passes. We validate the effectiveness and performance of our
approach on a range of benchmarks, expressing the secure compilation
of these applications in terms of observations to be made at
specific program points.