My research is to advance the state of the art of formal methods for correctness and security of computer systems, especially cyber-physical systems (CPSs), and to develop tools and techniques to help construct systems that are correct and secure. Formal methods are crucial for security goals, because they can show that no attack strategy will cause a system to misbehave. For the past several years, my research approach is to investigate sound, powerful, and pragmatic formal reasoning techniques for safety and security properties, and develop efficient enforcement mechanisms of these properties in constructing practical systems.