Memory-Safe Elimination of Side Channels
Resumo
In this project, we find a new service for partial control-flow linearization (PCFL), a code transformation initially conceived to maximize work performed in vectorized programs. We show that PCFL can be employed as a defense mechanism against timing attacks. This transformation is sound: given an instance of its public inputs, the partially linearized program always runs the same sequence of instructions, regardless of secret inputs. Incidentally, if the original program is publicly safe, then accesses to the data cache will be data oblivious in the transformed code. The transformation is optimal: every branch that depends on some secret data is linearized; no branch that depends on only public data is linearized. Therefore, the transformation preserves loops that depend exclusively on public information. If every branch that leaves a loop depends on secret data, then the transformed program will not terminate. Our transformation extends previous work in non-trivial ways. It handles C constructs such as “break”, “switch” and “continue”, which are absent in the FaCT domain-specific language (2018). Like Constantine (2021), our code transformation ensures operation invariance, but without requiring profiling information. Additionally, in contrast to SC-Eliminator (2018), our implementation handles programs containing general, unbounded loops.
Referências
Almeida, J. B., Barbosa, M., Barthe, G., Dupressoir, F., and Emmi, M. (2016). Verifying constant-time implementations. In SEC, page 53–70, USA. USENIX Association.
Almeida, J. B., Barbosa, M., Barthe, G., Grégoire, B., Koutsos, A., Laporte, V., Oliveira, T., and Strub, P. (2020). The last mile: High-assurance and high-speed cryptographic implementations. In Security & Privacy, pages 965–982, New York, NY, USA. IEEE.
Barthe, G., Blazy, S., Grégoire, B., Hutin, R., Laporte, V., Pichardie, D., and Trieu, A. (2019). Formal verification of a constant-time preserving C compiler. Proc. ACM Program. Lang., 4(POPL).
Borrello, P., D’Elia, D. C., Querzoni, L., and Giuffrida, C. (2021). Constantine: Automatic side-channel resistance using efficient control and data flow linearization. In CCS, page 715–733, New York, NY, USA. Association for Computing Machinery.
Cauligi, S., Soeller, G., Johannesmeyer, B., Brown, F., Wahby, R. S., Renner, J., Grégoire, B., Barthe, G., Jhala, R., and Stefan, D. (2019). Fact: A dsl for timing-sensitive computation. In PLDI, page 174–189, New York, NY, USA. Association for Computing Machinery.
Chattopadhyay, S. and Roychoudhury, A. (2018). Symbolic verification of cache side-channel freedom. Transactions on Computer-Aided Design of Integrated Circuits and Systems, 37(11):2812–2823.
Cleemput, J. V., Coppens, B., and De Sutter, B. (2012). Compiler mitigations for time attacks on modern x86 processors. Trans. Archit. Code Optim., 8(4).
Fell, A., Pham, H. T., and Lam, S.-K. (2019). Tad: Time side-channel attack defense of obfuscated source code. In ASP-DAC, page 58–63, New York, NY, USA. Association for Computing Machinery.
Ferrante, J. and Mace, M. (1985). On linearizing parallel code. In PLDI, page 179–190, New York, NY, USA. Association for Computing Machinery.
Flynn, M. J. (1972). Some computer organizations and their effectiveness. Transactions on Computers, 21(9):948–960.
Gruss, D., Lettner, J., Schuster, F., Ohrimenko, O., Haller, I., and Costa, M. (2017). Strong and efficient cache side-channel protection using hardware transactional memory. In SEC, page 217–233, USA. USENIX Association.
Guarnieri, M., Köpf, B., Reineke, J., and Vila, P. (2021). Hardware-software contracts for secure speculation. In Security & Privacy, pages 1868–1883, New York, US. IEEE.
Karrenberg, R. and Hack, S. (2012). Improving performance of opencl on cpus. In CC, page 1–20, Berlin, Heidelberg. Springer-Verlag.
Kocher, P. C. (1996). Timing attacks on implementations of diffie-hellman, rsa, dss, and other systems. In CRYPTO, page 104–113, Berlin, Heidelberg. Springer-Verlag.
Langley, A. (2010). Ctgrind—checking that functions are constant time with valgrind.
Lattner, C. and Adve, V. (2004). LLVM: A compilation framework for lifelong program analysis and transformation. In CGO, page 75, Washington, USA. IEEE Computer Society.
Moll, S. and Hack, S. (2018). Partial control-flow linearization. In PLDI, page 543–556, New York, NY, USA. Association for Computing Machinery.
Moreira, R. E., Collange, C., and Quintão Pereira, F. M. (2017). Function call revectorization. In PPoPP, page 313–326, New York, NY, USA. Association for Computing Machinery.
Ngo, V. C., Dehesa-Azuara, M., Fredrikson, M., and Hoffmann, J. (2017). Verifying and synthesizing constant-resource implementations with types. In Security and Privacy, pages 710–728, Washington, DC, USA. IEEE.
Reparaz, O., Balasch, J., and Verbauwhede, I. (2017). Dude, is my code constant time? In DATE, page 1701–1706, Leuven, BEL. European Design and Automation Association.
Rice, H. G. (1953). Classes of recursively enumerable sets and their decision problems. Transactions of the American Mathematical Society, 74(2):358–366.
Soares, L. and Pereira, F. M. Q. a. (2021). Memory-safe elimination of side channels. In CGO, pages 200–210, Washington, USA. IEEE.
Soares, L. D. C. (2022). Memory-safe elimination of side-channels. Master’s thesis, UFMG, Computer Science Department. Online available at: http://hdl.handle.net/1843/42564.
Sperle Campos, V. H., Alves, P. R., Nazaré Santos, H., and Quintão Pereira, F. M. (2016). Restrictification of function arguments. In CC, page 163–173, New York, NY, USA. Association for Computing Machinery.
Tizpaz-Niari, S., Černý, P., and Trivedi, A. (2019). Quantitative mitigation of timing side channels. In CAV, pages 140–160, Heidelberg, Germany. Springer.
Van Cleemput, J., De Sutter, B., and De Bosschere, K. (2020). Adaptive compiler strategies for mitigating timing side channel attacks. Transactions on Dependable and Secure Computing, 17(1):35–49.
Wu, M., Guo, S., Schaumont, P., and Wang, C. (2018). Eliminating timing side-channel leaks using program repair. In ISSTA, page 15–26, New York, NY, USA. Association for Computing Machinery.
