In this talk, I will present a technique to help software developersidentify potential vulnerabilities that can lead to cache-based timingattacks. Our technique leverages symbolic execution and constraintsolving to detect potential cache differences at each programpoint. We adopt a cache model that is general enough to capturevarious threat models that are employed in practical timing attacks.