Security-critical versus safety-critical software

Significant knowledge exists in the field of safety-critical software design and implementation. Formal design methods and high quality compilers allow production of software products with desired behavioral parameters. Generally, if we know what behavior parameters are needed then we can achieve them in the software code. But do we know what behavioral parameters are needed for security-critical software? Can application security be specified in a way suitable for the machine code so that we can achieve software that is as secure as it is safe?