×

Output-sensitive information flow analysis. (English) Zbl 1509.94041

Summary: Constant-time programming is a countermeasure to prevent cache based attacks where programs should not perform memory accesses that depend on secrets. In some cases this policy can be safely relaxed if one can prove that the program does not leak more information than the public outputs of the computation.
We propose a novel approach for verifying constant-time programming based on a new information flow property, called output-sensitive noninterference. Noninterference states that a public observer cannot learn anything about the private data. Since real systems need to intentionally declassify some information, this property is too strong in practice. In order to take into account public outputs we proceed as follows: instead of using complex explicit declassification policies, we partition variables in three sets: input, output and leakage variables. Then, we propose a typing system to statically check that leakage variables do not leak more information about the secret inputs than the public normal output. The novelty of our approach is that we track the dependence of leakage variables with respect not only to the initial values of input variables (as in classical approaches for noninterference), but taking also into account the final values of output variables. We adapted this approach to LLVM IR and we developed a prototype to verify LLVM implementations.

MSC:

94A15 Information theory (general)
68Q60 Specification and verification (program logics, model checking, etc.)
PDFBibTeX XMLCite
Full Text: arXiv Link

References:

[1] Agat, J.: Transforming out timing leaks. In: Proceedings of the 27th ACM SIGPLAN-SIGACT symposium on Principles of programming languages. pp. 40-53. ACM (2000) · Zbl 1323.68399
[2] Al Fardan, N.J., Paterson, K.G.: Lucky thirteen: Breaking the tls and dtls record protocols. In: Security and Privacy (SP), 2013 IEEE Symposium on. pp. 526-540. IEEE (2013)
[3] Albrecht, M.R., Paterson, K.G.: Lucky microseconds: A timing attack on amazon’s s2n implementation of tls. In: Annual International Conference on the Theory and Applications of Cryptographic Techniques. pp. 622-643. Springer (2016) · Zbl 1385.94004
[4] Almeida, J.B., Barbosa, M., Barthe, G., Dupressoir, F., Emmi, M.: Verifying constant-time implementations. In: 25th USENIX Security Symposium (USENIX Security 16). pp. 53-70. USENIX Association, Austin, TX (2016),https://www.usenix.org/conference/usenixsecurity16/technical-sessions/ presentation/almeida · Zbl 1387.94064
[5] Barnett, M., Chang, B.Y.E., DeLine, R., Jacobs, B., Leino, K.R.M.: Boogie: A modular reusable verifier for object-oriented programs. In: FMCO. vol. 5, pp. 364-387. Springer (2005)
[6] Barthe, G., Betarte, G., Campo, J., Luna, C., Pichardie, D.: System-level non-interference for constanttime cryptography. In: Proceedings of the 2014 ACM SIGSAC Conference on Computer and Communications Security. pp. 1267-1279. ACM (2014)
[7] Barthe, G., D’Argenio, P.R., Rezk, T.: Secure information flow by self-composition. In: Computer Security Foundations Workshop, 2004. Proceedings. 17th IEEE. pp. 100-114. IEEE (2004)
[8] Barthe, G., Rezk, T.: Secure information flow for a sequential java virtual machine. In: TLDI’05: Types in Language Design and Implementation. Citeseer (2003)
[9] Barthe, G., Rezk, T., Basu, A.: Security types preserving compilation. Computer Languages, Systems & Structures33(2), 35-59 (2007) · Zbl 1109.68025
[10] Bernstein, D., Lange, T., Schwabe, P.: The security impact of a new cryptographic library. Progress in Cryptology-LATINCRYPT 2012 pp. 159-176 (2012) · Zbl 1303.94067
[11] Blazy, S., Pichardie, D., Trieu, A.: Verifying constant-time implementations by abstract interpretation. In: European Symposium on Research in Computer Security. pp. 260-277. Springer (2017) · Zbl 1496.68100
[12] Brumley, D., Boneh, D.: Remote timing attacks are practical. Computer Networks48(5), 701-716 (2005)
[13] Choi, J.D., Cytron, R., Ferrante, J.: Automatic construction of sparse data flow evaluation graphs. In: Proceedings of the 18th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. pp. 55-66. POPL ’91, ACM (1991)
[14] Doychev, G., K¨opf, B., Mauborgne, L., Reineke, J.: Cacheaudit: A tool for the static analysis of cache side channels. ACM Trans. Inf. Syst. Secur.18(1), 4:1-4:32 (Jun 2015). https://doi.org/10.1145/2756550, http://doi.acm.org/10.1145/2756550
[15] Ferrante, J., Ottenstein, K., Warren, J.: The program dependence graph and its use in optimization. TOPLAS9(3), 319-349 (1987) · Zbl 0623.68012
[16] Genaim, S., Spoto, F.: Information flow analysis for java bytecode. In: Verification, Model Checking, and Abstract Interpretation. pp. 346-362. Springer (2005) · Zbl 1111.68505
[17] Gullasch, D., Bangerter, E., Krenn, S.: Cache games-bringing access-based cache attacks on aes to practice. In: Security and Privacy (SP), 2011 IEEE Symposium on. pp. 490-505. IEEE (2011)
[18] Hedin, D., Sands, D.: Timing aware information flow security for a javacard-like bytecode. Electronic Notes in Theoretical Computer Science141(1), 163-182 (2005)
[19] Hunt, S., Sands, D.: Binding time analysis: A new perspective. In: In Proceedings of the ACM Symposium on Partial Evaluation and Semantics-Based Program Manipulation (PEPM’91). pp. 154-164. ACM Press (1991)
[20] Hunt, S., Sands, D.: On flow-sensitive security types. In: ACM SIGPLAN Notices. vol. 41, pp. 79-90. ACM (2006) · Zbl 1370.68053
[21] Lattner, C., Adve, V.: Llvm: A compilation framework for lifelong program analysis & transformation. In: Proceedings of the International Symposium on Code Generation and Optimization: Feedback-directed and Runtime Optimization. CGO ’04, IEEE Computer Society, Washington, DC, USA (2004)
[22] Li, P., Zdancewic, S.: Downgrading policies and relaxed noninterference. In: Proceedings of POPL. vol. 40, pp. 158-170. ACM (2005) · Zbl 1369.68146
[23] Molnar, D., Piotrowski, M., Schultz, D., Wagner, D.: The program counter security model: Automatic detection and removal of control-flow side channel attacks. In: ICISC. vol. 3935, pp. 156-168. Springer · Zbl 1185.94061
[24] Myers, A.C.: Jflow: Practical mostly-static information flow control. In: Proceedings of the 26th ACM SIGPLAN-SIGACT symposium on Principles of programming languages. pp. 228-241. ACM (1999)
[25] Nation, J.B.: Notes on lattice theory (1998)
[26] Rodrigues, B., Quint˜ao Pereira, F.M., Aranha, D.F.: Sparse representation of implicit flows with applications to side-channel detection. In: Proceedings of the 25th International Conference on Compiler Construction. pp. 110-120. ACM (2016)
[27] Sabelfeld, A., Myers, A.C.: Language-based information-flow security. IEEE Journal on selected areas in communications21(1), 5-19 (2003)
[28] Sabelfeld, A., Sands, D.: Declassification: Dimensions and principles. Journal of Computer Security 17(5), 517-548 (2009)
[29] Swamy, N., Chen, J., Chugh, R.: Enforcing stateful authorization and information flow policies in fine. In: ESOP. pp. 529-549. Springer (2010)
[30] Vaughan, J.A., Zdancewic, S.: A cryptographic decentralized label model. In: Security and Privacy, 2007. SP’07. IEEE Symposium on. pp. 192-206. IEEE (2007)
[31] Volpano, D., Irvine, C., Smith, G.: A sound type system for secure flow analysis. Journal of computer security4(2-3), 167-187 (1996)
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.