{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T16:07:17Z","timestamp":1725552437126},"publisher-location":"Berlin, Heidelberg","reference-count":30,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642124587"},{"type":"electronic","value":"9783642124594"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2010]]},"DOI":"10.1007\/978-3-642-12459-4_9","type":"book-chapter","created":{"date-parts":[[2010,4,29]],"date-time":"2010-04-29T02:49:38Z","timestamp":1272509378000},"page":"111-125","source":"Crossref","is-referenced-by-count":5,"title":["Specification and Verification of Side Channel Declassification"],"prefix":"10.1007","author":[{"given":"Josef","family":"Svenningsson","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"David","family":"Sands","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"9_CR1","doi-asserted-by":"crossref","unstructured":"Agat, J.: Transforming out timing leaks. In: Proc. ACM Symp. on Principles of Programming Languages, January 2000, pp. 40\u201353 (2000)","DOI":"10.1145\/325694.325702"},{"key":"9_CR2","unstructured":"Agat, J., Sands, D.: On confidentiality and algorithms. In: Proc. IEEE Symp. on Security and Privacy, May 2001, pp. 64\u201377 (2001)"},{"key":"9_CR3","first-page":"701","volume":"48","author":"D. Brumley","year":"2005","unstructured":"Brumley, D., Boneh, D.: Remote timing attacks are practical. Journal of Computer and Telecommunications Networking\u00a048, 701\u2013716 (2005)","journal-title":"Journal of Computer and Telecommunications Networking"},{"key":"9_CR4","series-title":"Lecture Notes in Computer Science","first-page":"100","volume-title":"Proceedings of CSFW 2004","author":"G. Barthe","year":"2004","unstructured":"Barthe, G., D\u2019Argenio, P., Rezk, T.: Secure information flow by self-composition. In: Proceedings of CSFW 2004. LNCS, pp. 100\u2013114. IEEE Press, Los Alamitos (2004)"},{"issue":"6","key":"9_CR5","doi-asserted-by":"publisher","first-page":"760","DOI":"10.1109\/TC.2004.13","volume":"53","author":"B. Chevallier-Mames","year":"2004","unstructured":"Chevallier-Mames, B., Ciet, M., Joye, M.: Low-cost solutions for preventing simple sidechannel analysis: Side-channel atomicity. IEEE Transactions on Computers\u00a053(6), 760\u2013768 (2004)","journal-title":"IEEE Transactions on Computers"},{"key":"9_CR6","doi-asserted-by":"crossref","unstructured":"Coron, J.-S.: Resistance against differential power analysis for elliptic curve cryptosystems. In: Koc, C.K., Paar, C. (eds.) Cryptographic Hardware and Embedded Systems, pp. 292\u2013302 (1999)","DOI":"10.1007\/3-540-48059-5_25"},{"key":"9_CR7","unstructured":"Darvas, A., H\u00e4hnle, R., Sands, D.: A theorem proving approach to analysis of secure information flow. In: Proc. Workshop on Issues in the Theory of Security (April 2003)"},{"key":"9_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"81","DOI":"10.1007\/978-3-540-88625-9_6","volume-title":"Information and Communications Security","author":"A. Pierro Di","year":"2008","unstructured":"Di Pierro, A., Hankin, C., Wiklicky, H.: Quantifying timing leaks and cost optimisation. In: Chen, L., Ryan, M.D., Wang, G. (eds.) ICICS 2008. LNCS, vol.\u00a05308, pp. 81\u201396. Springer, Heidelberg (2008)"},{"key":"9_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"289","DOI":"10.1007\/11603009_22","volume-title":"Formal Modeling and Analysis of Timed Systems","author":"R. Giacobazzi","year":"2005","unstructured":"Giacobazzi, R., Mastroeni, I.: Timed abstract non-interference. In: Pettersson, P., Yi, W. (eds.) FORMATS 2005. LNCS, vol.\u00a03829, pp. 289\u2013303. Springer, Heidelberg (2005)"},{"key":"9_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"474","DOI":"10.1007\/11691372_34","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"B.S. Gulavani","year":"2006","unstructured":"Gulavani, B.S., Rajamani, S.K.: Counterexample driven refinement for abstract interpretation. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006. LNCS, vol.\u00a03920, pp. 474\u2013488. Springer, Heidelberg (2006)"},{"key":"9_CR11","unstructured":"Hedin, D.: Program analysis issues in language based security. PhD thesis, Department of Computer Science and Engineering, Chalmers University of Technology (2008)"},{"key":"9_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"235","DOI":"10.1007\/3-540-44829-2_17","volume-title":"Model Checking Software","author":"T.A. Henzinger","year":"2003","unstructured":"Henzinger, T.A., Jhala, R., Majumdar, R., Sutre, G.: Software verification with blast. In: Ball, T., Rajamani, S.K. (eds.) SPIN 2003. LNCS, vol.\u00a02648, pp. 235\u2013239. Springer, Heidelberg (2003)"},{"key":"9_CR13","doi-asserted-by":"crossref","unstructured":"Hedin, D., Sands, D.: Timing aware information flow security for a JavaCard-like bytecode. In: First Workshop on Bytecode Semantics, Verification, Analysis and Transformation (BYTECODE 2005). Electronic Notes in Theoretical Computer Science (2005) (to appear)","DOI":"10.1016\/j.entcs.2005.02.031"},{"key":"9_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"243","DOI":"10.1007\/11863908_16","volume-title":"Computer Security \u2013 ESORICS 2006","author":"B. K\u00f6pf","year":"2006","unstructured":"K\u00f6pf, B., Basin, D.A.: Timing-sensitive information flow analysis for synchronous systems. In: Gollmann, D., Meier, J., Sabelfeld, A. (eds.) ESORICS 2006. LNCS, vol.\u00a04189, pp. 243\u2013262. Springer, Heidelberg (2006)"},{"key":"9_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"388","DOI":"10.1007\/3-540-48405-1_25","volume-title":"Advances in Cryptology - CRYPTO \u201999","author":"P. Kocher","year":"1999","unstructured":"Kocher, P., Jaffe, J., Jun, B.: Differential power analysis. In: Wiener, M. (ed.) CRYPTO 1999. LNCS, vol.\u00a01666, pp. 388\u2013397. Springer, Heidelberg (1999)"},{"key":"9_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"47","DOI":"10.1007\/11679219_5","volume-title":"Formal Aspects in Security and Trust","author":"B. K\u00f6pf","year":"2006","unstructured":"K\u00f6pf, B., Mantel, H.: Eliminating implicit information leaks by transformational typing and unification. In: Dimitrakos, T., Martinelli, F., Ryan, P.Y.A., Schneider, S. (eds.) FAST 2005. LNCS, vol.\u00a03866, pp. 47\u201362. Springer, Heidelberg (2006)"},{"key":"9_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"104","DOI":"10.1007\/3-540-68697-5_9","volume-title":"Advances in Cryptology - CRYPTO \u201996","author":"P.C. Kocher","year":"1996","unstructured":"Kocher, P.C.: Timing attacks on implementations of Diffie-Hellman, RSA, DSS, and other systems. In: Koblitz, N. (ed.) CRYPTO 1996. LNCS, vol.\u00a01109, pp. 104\u2013113. Springer, Heidelberg (1996)"},{"issue":"10","key":"9_CR18","doi-asserted-by":"publisher","first-page":"613","DOI":"10.1145\/362375.362389","volume":"16","author":"B.W. Lampson","year":"1973","unstructured":"Lampson, B.W.: A note on the confinement problem. Comm. of the ACM\u00a016(10), 613\u2013615 (1973)","journal-title":"Comm. of the ACM"},{"key":"9_CR19","doi-asserted-by":"crossref","unstructured":"Li, P., Zdancewic, S.: Downgrading policies and relaxed noninterference. In: Proc. ACM Symp. on Principles of Programming Languages, January 2005, pp. 158\u2013170 (2005)","DOI":"10.1145\/1040305.1040319"},{"key":"9_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"144","DOI":"10.1007\/3-540-48059-5_14","volume-title":"Cryptographic Hardware and Embedded Systems","author":"T.S. Messergers","year":"1999","unstructured":"Messergers, T.S., Dabbish, E.A., Sloan, R.H.: Power analysis attacks on modular exponentiation in smartcards, in cryptographic hardware and embedded systems. In: Ko\u00e7, \u00c7.K., Paar, C. (eds.) CHES 1999. LNCS, vol.\u00a01717, pp. 144\u2013157. Springer, Heidelberg (1999)"},{"key":"9_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"156","DOI":"10.1007\/11734727_14","volume-title":"Information Security and Cryptology - ICISC 2005","author":"D. Molnar","year":"2006","unstructured":"Molnar, D., Piotrowski, M., Schultz, D., Wagner, D.: The program counter security model: Automatic detection and removal of control-flow side channel attacks. In: Won, D.H., Kim, S. (eds.) ICISC 2005. LNCS, vol.\u00a03935, pp. 156\u2013168. Springer, Heidelberg (2006)"},{"key":"9_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"78","DOI":"10.1007\/3-540-44499-8_6","volume-title":"Cryptographic Hardware and Embedded Systems - CHES 2000","author":"R. Mayer-Sommer","year":"2000","unstructured":"Mayer-Sommer, R.: Smartly analyzing the simplicity and the power of simple power analysis on smartcards. In: Paar, C., Ko\u00e7, \u00c7.K. (eds.) CHES 2000. LNCS, vol.\u00a01965, pp. 78\u201392. Springer, Heidelberg (2000)"},{"key":"9_CR23","doi-asserted-by":"crossref","unstructured":"Puschner, P., Burns, A.: Writing temporally predictable code. In: 7th IEEE International Workshop on Object-Oriented Real-Time Dependable Systems (2002)","DOI":"10.1109\/WORDS.2002.1000040"},{"issue":"2","key":"9_CR24","doi-asserted-by":"publisher","first-page":"173","DOI":"10.1016\/j.jlap.2007.02.007","volume":"72","author":"A. Pierro Di","year":"2007","unstructured":"Di Pierro, A., Hankin, C., Siveroni, I., Wiklicky, H.: Tempus fugit: How to plug it. J. Log. Algebr. Program.\u00a072(2), 173\u2013190 (2007)","journal-title":"J. Log. Algebr. Program."},{"issue":"1","key":"9_CR25","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1109\/JSAC.2002.806121","volume":"21","author":"A. Sabelfeld","year":"2003","unstructured":"Sabelfeld, A., Myers, A.C.: Language-based information-flow security. IEEE J. Selected Areas in Communications\u00a021(1), 5\u201319 (2003)","journal-title":"IEEE J. Selected Areas in Communications"},{"key":"9_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"174","DOI":"10.1007\/978-3-540-37621-7_9","volume-title":"Software Security - Theories and Systems","author":"A. Sabelfeld","year":"2004","unstructured":"Sabelfeld, A., Myers, A.C.: A model for delimited information release. In: Futatsugi, K., Mizoguchi, F., Yonezaki, N. (eds.) ISSS 2003. LNCS, vol.\u00a03233, pp. 174\u2013191. Springer, Heidelberg (2004)"},{"key":"9_CR27","doi-asserted-by":"crossref","unstructured":"Sabelfeld, A., Sands, D.: Probabilistic noninterference for multi-threaded programs. In: Proc. IEEE Computer Security Foundations Workshop, July 2000, pp. 200\u2013214 (2000)","DOI":"10.1109\/CSFW.2000.856937"},{"key":"9_CR28","first-page":"255","volume-title":"Proceedings of the 18th IEEE Computer Security Foundations Workshop","author":"A. Sabelfeld","year":"2005","unstructured":"Sabelfeld, A., Sands, D.: Dimensions and principles of declassification. In: Proceedings of the 18th IEEE Computer Security Foundations Workshop, Cambridge, England, pp. 255\u2013269. IEEE Computer Society Press, Los Alamitos (2005)"},{"key":"9_CR29","unstructured":"Svenningsson, J., Sands, D.: Specification and verification of side channel declassification. Technical Report 2009:13, Department of Computer Science and Engineering, Chalmers University of Technology and University of Gothenburg (December 2009) arXiv:0912.2952 (cs.CR)"},{"key":"9_CR30","doi-asserted-by":"crossref","unstructured":"Terauchi, T., Aiken, A.: Secure information flow as a safety problem. In: Proceedings of the 12th International Static Analysis Symposium, pp. 352\u2013367 (2005)","DOI":"10.1007\/11547662_24"}],"container-title":["Lecture Notes in Computer Science","Formal Aspects in Security and Trust"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-12459-4_9.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,30]],"date-time":"2021-04-30T07:41:48Z","timestamp":1619768508000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-12459-4_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9783642124587","9783642124594"],"references-count":30,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-12459-4_9","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2010]]}}}