Our paper, “Verifying and Synthesizing Constant-Resource Implementations with Types” (with Mario Dehesa-Azuara, Matthew Fredrikson, and Jan Hoffmann), will appear in the 2017 IEEE Symposium on Security & Privacy (Oakland). The paper, technical report, and code can be obtained here.
This work presents a type-based techniques for enforcing non-interference property and constant-resource usage in functional programs. The goal is to dectect and prevent side channels allowing attackers to derive information about secret data by observing the covert channels.