Described is a system for translating security objectives to properties of software code. The system receives a software code and a description of user security objectives written in a high-level language. Using a set of inference rules, the user security objective is translated into a formal security objective. The formal security objective is adapted into a low-level property to fit a target program having software code. Finally, it is determined whether the user objective has been satisfied by analyzing the software code with respect to the low-level property.