{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T13:50:44Z","timestamp":1725544244489},"publisher-location":"Berlin, Heidelberg","reference-count":29,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540336891"},{"type":"electronic","value":"9783540336914"}],"license":[{"start":{"date-parts":[[2006,1,1]],"date-time":"2006-01-01T00:00:00Z","timestamp":1136073600000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2006]]},"DOI":"10.1007\/11741060_3","type":"book-chapter","created":{"date-parts":[[2006,4,27]],"date-time":"2006-04-27T09:42:07Z","timestamp":1146130927000},"page":"37-56","source":"Crossref","is-referenced-by-count":8,"title":["Information Flow Analysis for a Typed Assembly Language with Polymorphic Stacks"],"prefix":"10.1007","author":[{"given":"Eduardo","family":"Bonelli","sequence":"first","affiliation":[]},{"given":"Adriana","family":"Compagnoni","sequence":"additional","affiliation":[]},{"given":"Ricardo","family":"Medel","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"issue":"3-4","key":"3_CR1","doi-asserted-by":"publisher","first-page":"261","DOI":"10.1023\/B:JARS.0000021014.79255.33","volume":"31","author":"D. Aspinall","year":"2003","unstructured":"Aspinall, D., Compagnoni, A.B.: Heap bounded assembly language. Journal of Automated Reasoning, Special Issue on Proof-Carrying Code\u00a031(3-4), 261\u2013302 (2003)","journal-title":"Journal of Automated Reasoning, Special Issue on Proof-Carrying Code"},{"key":"3_CR2","unstructured":"Banerjee, A., Naumann, D.: Secure information flow and pointer confinement in a Java-like language. In: Proceedings of Fifteenth IEEE Computer Security Foundations - CSFW, June 2002, pp. 253\u2013267 (2002)"},{"key":"3_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1007\/978-3-540-24622-0_2","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"G. Barthe","year":"2004","unstructured":"Barthe, G., Basu, A., Rezk, T.: Security types preserving compilation. In: Steffen, B., Levi, G. (eds.) VMCAI 2004. LNCS, vol.\u00a02937, pp. 2\u201315. Springer, Heidelberg (2004)"},{"key":"3_CR4","unstructured":"Bell, D., LaPadula, L.: Secure computer systems: Mathematical foundations and model. Technical Report MTR 2547 v2, MITRE (November 1973)"},{"key":"3_CR5","unstructured":"Biba, K.: Integrity considerations for secure computer systems. Technical Report ESD-TR-76-372, USAF Electronic Systems Division, Bedford, MA (April 1977)"},{"key":"3_CR6","doi-asserted-by":"crossref","unstructured":"Bonelli, E., Compagnoni, A., Medel, R.: Information flow analysis for a typed assembly language with polymorphic stacks (2005), http:\/\/www.cs.stevens.edu\/~rmedel\/siftalTechReport.ps","DOI":"10.1007\/11741060_3"},{"key":"3_CR7","unstructured":"Bonelli, E., Compagnoni, A., Medel, R.: SIFTAL: A typed assembly language for secure information flow analysis (2005), http:\/\/www.cs.stevens.edu\/~rmedel\/techReport.ps"},{"key":"3_CR8","doi-asserted-by":"crossref","unstructured":"Chothia, T., Duggan, D., Vitek, J.: Type-based distributed access control. In: Proc. of IEEE Computer Security Foundations Workshop, Asilomar, California (2003)","DOI":"10.1109\/CSFW.2003.1212712"},{"key":"3_CR9","unstructured":"Crary, K., Kliger, A., Pfenning, F.: A monadic analysis of information flow security with mutable state. Technical Report CMU-CS-03-164, Carnegie Mellon University (September 2003)"},{"issue":"5","key":"3_CR10","doi-asserted-by":"publisher","first-page":"236","DOI":"10.1145\/360051.360056","volume":"19","author":"D.E. Denning","year":"1976","unstructured":"Denning, D.E.: A lattice model of secure information flow. Communications of the ACM\u00a019(5), 236\u2013242 (1976)","journal-title":"Communications of the ACM"},{"issue":"7","key":"3_CR11","doi-asserted-by":"publisher","first-page":"504","DOI":"10.1145\/359636.359712","volume":"20","author":"D.E. Denning","year":"1977","unstructured":"Denning, D.E., Denning, P.J.: Certification of programs for secure information flow. Communications of the ACM\u00a020(7), 504\u2013513 (1977)","journal-title":"Communications of the ACM"},{"key":"3_CR12","doi-asserted-by":"crossref","unstructured":"Feiertag, R.J., Levitt, K.N., Robinson, L.: Proving multilevel security of a system design. In: 6th ACM Symp. Operating System Principles, November 1977, pp. 57\u201365 (1977)","DOI":"10.1145\/800214.806547"},{"key":"3_CR13","first-page":"11","volume-title":"Proceedings of the Symposium on Security and Privacy","author":"J.A. Goguen","year":"1982","unstructured":"Goguen, J.A., Meseguer, J.: Security policy and security models. In: Proceedings of the Symposium on Security and Privacy, pp. 11\u201320. IEEE Press, Los Alamitos (1982)"},{"key":"3_CR14","doi-asserted-by":"crossref","unstructured":"Hedin, D., Sands, D.: Timing aware information flow security for a JavaCard-like bytecode. In: Proceedings of the First Workshop on Bytecode Semantics, Verification, Analysis and Transformation (Bytecode 2005), December 2005. Electronic Notes in Theoretical Computer Science, vol.\u00a0141(1), pp. 163\u2013182 (2005)","DOI":"10.1016\/j.entcs.2005.02.031"},{"key":"3_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"360","DOI":"10.1007\/11560586_29","volume-title":"Theoretical Computer Science","author":"R. Medel","year":"2005","unstructured":"Medel, R., Compagnoni, A., Bonelli, E.: A typed assembly language for non-interference. In: Coppo, M., Lodi, E., Pinna, G.M. (eds.) ICTCS 2005. LNCS, vol.\u00a03701, pp. 360\u2013374. Springer, Heidelberg (2005)"},{"key":"3_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"28","DOI":"10.1007\/BFb0055511","volume-title":"Types in Compilation","author":"G. Morrisett","year":"1998","unstructured":"Morrisett, G., Crary, K., Glew, N., Walker, D.: Stack-based typed assembly language. In: Leroy, X., Ohori, A. (eds.) TIC 1998. LNCS, vol.\u00a01473, pp. 28\u201352. Springer, Heidelberg (1998)"},{"key":"#cr-split#-3_CR17.1","doi-asserted-by":"crossref","unstructured":"Morrisett, G., Walker, D., Crary, K., Glew, N.: From System F to Typed Assembly Language. ACM Transactions on Programming Languages and Systems??21(3), 528???569 (1999);","DOI":"10.1145\/319301.319345"},{"key":"#cr-split#-3_CR17.2","unstructured":"This is the expanded version of a paper that appeared in Twenty-Fifth ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, San Diego, CA, USA, pp. 85???97 (January 1998)"},{"key":"3_CR18","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. Myers","year":"2004","unstructured":"Myers, A., Sabelfeld, A.: 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":"3_CR19","doi-asserted-by":"crossref","unstructured":"Myers, A., Sabelfeld, A., Zdancewic, S.: Enforcing robust declassification. In: 7th IEEE Computer Security Foundations Workshop (2004)","DOI":"10.1109\/CSFW.2004.1310740"},{"key":"3_CR20","unstructured":"Necula, G.: Compiling with Proofs. PhD thesis, Carnegie Mellon University (September 1998)"},{"key":"3_CR21","first-page":"421","volume-title":"Proceedings of the 2nd International Conference on Software Engineering","author":"P.G. Neumman","year":"1976","unstructured":"Neumman, P.G., Feiertag, R.J., Levitt, K.N., Robinson, L.: Software development and proofs of multi-level security. In: Proceedings of the 2nd International Conference on Software Engineering, pp. 421\u2013428. IEEE Computer Society, Los Alamitos (1976)"},{"key":"3_CR22","doi-asserted-by":"crossref","unstructured":"Sabelfeld, A., Myers, A.: Language-based information-flow security. IEEE Journal on Selected Areas in Communications\u00a021(1) (2003)","DOI":"10.1109\/JSAC.2002.806121"},{"key":"3_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"366","DOI":"10.1007\/3-540-46425-5_24","volume-title":"Programming Languages and Systems","author":"F. Smith","year":"2000","unstructured":"Smith, F., Walker, D., Morrisett, G.: Alias types. In: Smolka, G. (ed.) ESOP 2000. LNCS, vol.\u00a01782, pp. 366\u2013381. Springer, Heidelberg (2000)"},{"key":"3_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"607","DOI":"10.1007\/BFb0030629","volume-title":"TAPSOFT\u201997: Theory and Practice of Software Development","author":"D.M. Volpano","year":"1997","unstructured":"Volpano, D.M., Smith, G.: A type-based approach to program security. In: Bidoit, M., Dauchet, M. (eds.) TAPSOFT 1997. LNCS, vol.\u00a01214, pp. 607\u2013621. Springer, Heidelberg (1997)"},{"key":"3_CR25","unstructured":"Xi, H., Harper, R.: A dependently typed assembly language. Technical Report OGI-CSE-99-008, Oregon Graduate Institute of Science and Technology (July 1999)"},{"key":"3_CR26","doi-asserted-by":"crossref","unstructured":"Yu, D., Islam, N.: A typed assembly language for confidentiality. Personal Communication (July 2005)","DOI":"10.1007\/11693024_12"},{"key":"3_CR27","doi-asserted-by":"crossref","unstructured":"Zdancewic, S., Myers, A.: Robust declassification. In: Proc. of 14th IEEE Computer Security Foundations Workshop, Cape Breton, Canada, June 2001, pp. 15\u201323 (2001)","DOI":"10.1109\/CSFW.2001.930133"},{"key":"3_CR28","doi-asserted-by":"crossref","unstructured":"Zdancewic, S., Myers, A.: Secure information flow via linear continuations. Higher Order and Symbolic Computation\u00a015(2\u20133) (2002)","DOI":"10.1023\/A:1020843229247"}],"container-title":["Lecture Notes in Computer Science","Construction and Analysis of Safe, Secure, and Interoperable Smart Devices"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11741060_3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,18]],"date-time":"2019-04-18T05:54:06Z","timestamp":1555566846000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11741060_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006]]},"ISBN":["9783540336891","9783540336914"],"references-count":29,"URL":"https:\/\/doi.org\/10.1007\/11741060_3","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2006]]}}}