{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,25]],"date-time":"2025-03-25T18:26:13Z","timestamp":1742927173135,"version":"3.40.3"},"publisher-location":"Cham","reference-count":31,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030299583"},{"type":"electronic","value":"9783030299590"}],"license":[{"start":{"date-parts":[[2019,1,1]],"date-time":"2019-01-01T00:00:00Z","timestamp":1546300800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2019,1,1]],"date-time":"2019-01-01T00:00:00Z","timestamp":1546300800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2019]]},"DOI":"10.1007\/978-3-030-29959-0_17","type":"book-chapter","created":{"date-parts":[[2019,9,14]],"date-time":"2019-09-14T23:04:10Z","timestamp":1568502250000},"page":"341-360","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["A Formal Model for Checking Cryptographic API Usage in JavaScript"],"prefix":"10.1007","author":[{"given":"Duncan","family":"Mitchell","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6517-1690","authenticated-orcid":false,"given":"Johannes","family":"Kinder","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2019,9,15]]},"reference":[{"issue":"2","key":"17_CR1","doi-asserted-by":"publisher","first-page":"8:1","DOI":"10.1145\/1890028.1890031","volume":"33","author":"J Bengtson","year":"2011","unstructured":"Bengtson, J., Bhargavan, K., Fournet, C., Gordon, A.D., Maffeis, S.: Refinement types for secure implementations. ACM Trans. Prog. Lang. Syst. 33(2), 8:1\u20138:45 (2011)","journal-title":"ACM Trans. Prog. Lang. Syst."},{"key":"17_CR2","doi-asserted-by":"crossref","unstructured":"Bhargavan, K., Blanchet, B., Kobeissi, N.: Verified models and reference implementations for the TLS 1.3 standard candidate. In: IEEE Symposium on Security and Privacy (S&P) (2017)","DOI":"10.1109\/SP.2017.26"},{"key":"17_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"88","DOI":"10.1007\/978-3-319-10082-1_4","volume-title":"Foundations of Security Analysis and Design VII","author":"K Bhargavan","year":"2014","unstructured":"Bhargavan, K., Delignat-Lavaud, A., Maffeis, S.: Defensive JavaScript \u2013 building and verifying secure web components. In: Aldini, A., Lopez, J., Martinelli, F. (eds.) FOSAD 2012-2013. LNCS, vol. 8604, pp. 88\u2013123. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-10082-1_4"},{"key":"17_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"47","DOI":"10.1007\/978-3-642-17164-2_5","volume-title":"Programming Languages and Systems","author":"K Bhargavan","year":"2010","unstructured":"Bhargavan, K., Fournet, C., Guts, N.: Typechecking higher-order security libraries. In: Ueda, K. (ed.) APLAS 2010. LNCS, vol. 6461, pp. 47\u201362. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-17164-2_5"},{"key":"17_CR5","doi-asserted-by":"crossref","unstructured":"Bhargavan, K., Fournet, C., Kohlweiss, M., Pironti, A., Strub, P.: Implementing TLS with verified cryptographic security. In: IEEE Symposium on Security and Privacy (S&P) (2013)","DOI":"10.1109\/SP.2013.37"},{"issue":"OOPSLA","key":"17_CR6","first-page":"48:1","volume":"1","author":"A Chaudhuri","year":"2017","unstructured":"Chaudhuri, A., Vekris, P., Goldman, S., Roch, M., Levi, G.: Fast and precise type checking for JavaScript. Proc. ACM Prog. Lang. 1(OOPSLA), 48:1\u201348:30 (2017)","journal-title":"Proc. ACM Prog. Lang."},{"key":"17_CR7","doi-asserted-by":"crossref","unstructured":"Chugh, R., Herman, D., Jhala, R.: Dependent types for JavaScript. In: ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA) (2012)","DOI":"10.1145\/2384616.2384659"},{"key":"17_CR8","doi-asserted-by":"crossref","unstructured":"Egele, M., Brumley, D., Fratantonio, Y., Kruegel, C.: An empirical study of cryptographic misuse in android applications. In: ACM SIGSAC Conference on Computer and Communications Security (CCS) (2013)","DOI":"10.1145\/2508859.2516693"},{"key":"17_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"126","DOI":"10.1007\/978-3-642-14107-2_7","volume-title":"ECOOP 2010 \u2013 Object-Oriented Programming","author":"A Guha","year":"2010","unstructured":"Guha, A., Saftoiu, C., Krishnamurthi, S.: The essence of JavaScript. In: D\u2019Hondt, T. (ed.) ECOOP 2010. LNCS, vol. 6183, pp. 126\u2013150. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-14107-2_7"},{"key":"17_CR10","doi-asserted-by":"crossref","unstructured":"Hedin, D., Birgisson, A., Bello, L., Sabelfeld, A.: JSFlow: tracking information flow in JavaScript and its APIs. In: ACM Symposium on Applied Computing (2014)","DOI":"10.1145\/2554850.2554909"},{"key":"17_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"49","DOI":"10.1007\/978-3-662-54455-6_3","volume-title":"Principles of Security and Trust","author":"D Hedin","year":"2017","unstructured":"Hedin, D., Sj\u00f6sten, A., Piessens, F., Sabelfeld, A.: A principled approach to tracking information flow in the presence of libraries. In: Maffei, M., Ryan, M. (eds.) POST 2017. LNCS, vol. 10204, pp. 49\u201370. Springer, Heidelberg (2017). https:\/\/doi.org\/10.1007\/978-3-662-54455-6_3"},{"key":"17_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"11","DOI":"10.1007\/978-3-662-46666-7_2","volume-title":"Principles of Security and Trust","author":"S Heule","year":"2015","unstructured":"Heule, S., Stefan, D., Yang, E.Z., Mitchell, J.C., Russo, A.: IFC inside: retrofitting languages with dynamic information flow control. In: Focardi, R., Myers, A. (eds.) POST 2015. LNCS, vol. 9036, pp. 11\u201331. Springer, Heidelberg (2015). https:\/\/doi.org\/10.1007\/978-3-662-46666-7_2"},{"key":"17_CR13","unstructured":"Keil, M., Thiemann, P.: TreatJS: higher-order contracts for JavaScripts. In: European Conference on Object-Oriented Programming (ECOOP) (2015)"},{"key":"17_CR14","doi-asserted-by":"crossref","unstructured":"Kobeissi, N., Bhargavan, K., Blanchet, B.: Automated verification for secure messaging protocols and their implementations: a symbolic and computational approach. In: IEEE European Symposium on Security and Privacy (EuroS&P) (2017)","DOI":"10.1109\/EuroSP.2017.38"},{"key":"17_CR15","unstructured":"Kr\u00fcger, S., Sp\u00e4th, J., Ali, K., Bodden, E., Mezini, M.: CrySL: validating correct usage of cryptographic APIs. In: European Conference on Object-Oriented Programming (ECOOP) (2018)"},{"key":"17_CR16","doi-asserted-by":"crossref","unstructured":"Lazar, D., Chen, H., Wang, X., Zeldovich, N.: Why does cryptographic software fail?: a case study and open problems. In: Asia-Pacific Workshop on Systems (2014)","DOI":"10.1145\/2637166.2637237"},{"key":"17_CR17","doi-asserted-by":"crossref","unstructured":"Loring, B., Mitchell, D., Kinder, J.: Sound regular expression semantics for dynamic symbolic execution of JavaScript. In: Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI). ACM (2019)","DOI":"10.1145\/3314221.3314645"},{"issue":"OOPSLA","key":"17_CR18","first-page":"861","volume":"1","author":"M Madsen","year":"2017","unstructured":"Madsen, M., Lhot\u00e1k, O., Tip, F.: A model for reasoning about JavaScript promises. Proc. ACM Prog. Lang. 1(OOPSLA), 861\u20138624 (2017)","journal-title":"Proc. ACM Prog. Lang."},{"key":"17_CR19","doi-asserted-by":"crossref","unstructured":"Mitchell, D., van Binsbergen, L.T., Loring, B., Kinder, J.: Checking cryptographic API usage with composable annotations. In: ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation (PEPM) (2018)","DOI":"10.1145\/3175493.3162071"},{"key":"17_CR20","doi-asserted-by":"crossref","unstructured":"Nadi, S., Kr\u00fcger, S., Mezini, M., Bodden, E.: Jumping through hoops: why do Java developers struggle with cryptography APIs? In: International Conference on Software Engineering (ICSE) (2016)","DOI":"10.1145\/2884781.2884790"},{"key":"17_CR21","doi-asserted-by":"crossref","unstructured":"Park, D., Stef\u0103nescu, A., Ro\u015fu, G.: KJS: a complete formal semantics of JavaScript. In: ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI) (2015)","DOI":"10.1145\/2737924.2737991"},{"key":"17_CR22","doi-asserted-by":"crossref","unstructured":"Politz, J.G., Carroll, M.J., Lerner, B.S., Pombrio, J., Krishnamurthi, S.: A tested semantics for getters, setters, and eval in JavaScript. In: Symposium on Dynamic Languages (DLS) (2012)","DOI":"10.1145\/2384577.2384579"},{"key":"17_CR23","doi-asserted-by":"crossref","unstructured":"Rastogi, A., Swamy, N., Fournet, C., Bierman, G.M., Vekris, P.: Safe & efficient gradual typing for TypeScript. In: ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL) (2015)","DOI":"10.1145\/2676726.2676971"},{"issue":"1","key":"17_CR24","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. Sel. Areas Commun. 21(1), 5\u201319 (2003)","journal-title":"IEEE J. Sel. Areas Commun."},{"issue":"POPL","key":"17_CR25","first-page":"501","volume":"2","author":"JF Santos","year":"2018","unstructured":"Santos, J.F., Maksimovic, P., Naudziuniene, D., Wood, T., Gardner, P.: JaVerT: JavaScript verification toolchain. Proc. ACM Program. Lang. 2(POPL), 501\u20135033 (2018)","journal-title":"Proc. ACM Program. Lang."},{"key":"17_CR26","series-title":"IFIP Advances in Information and Communication Technology","doi-asserted-by":"publisher","first-page":"278","DOI":"10.1007\/978-3-642-55415-5_23","volume-title":"ICT Systems Security and Privacy Protection","author":"JF Santos","year":"2014","unstructured":"Santos, J.F., Rezk, T.: An information flow monitor-inlining compiler for securing a core of JavaScript. In: Cuppens-Boulahia, N., Cuppens, F., Jajodia, S., Abou El Kalam, A., Sans, T. (eds.) SEC 2014. IAICT, vol. 428, pp. 278\u2013292. Springer, Heidelberg (2014). https:\/\/doi.org\/10.1007\/978-3-642-55415-5_23"},{"key":"17_CR27","unstructured":"Stefan, D., et al.: Protecting users by confining JavaScript with COWL. In: USENIX Symposium on Operating Systems Design and Implementation (OSDI) (2014)"},{"key":"17_CR28","doi-asserted-by":"crossref","unstructured":"Swamy, N., Chen, J., Fournet, C., Strub, P., Bhargavan, K., Yang, J.: Secure distributed programming with value-dependent types. In: ACM SIGPLAN International Conference on Functional Programming (ICFP) (2011)","DOI":"10.1145\/2034773.2034811"},{"key":"17_CR29","doi-asserted-by":"crossref","unstructured":"Taly, A., Erlingsson, \u00da., Mitchell, J.C., Miller, M.S., Nagra, J.: Automated analysis of security-critical JavaScript APIs. In: IEEE Symposium on Security and Privacy (S&P) (2011)","DOI":"10.1109\/SP.2011.39"},{"key":"17_CR30","doi-asserted-by":"crossref","unstructured":"Vekris, P., Cosman, B., Jhala, R.: Refinement types for TypeScript. In: ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI) (2016)","DOI":"10.1145\/2908080.2908110"},{"key":"17_CR31","unstructured":"Watson, M.: Web cryptography API. W3C recommendation, W3C, January 2017"}],"container-title":["Lecture Notes in Computer Science","Computer Security \u2013 ESORICS 2019"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-29959-0_17","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,9,15]],"date-time":"2024-09-15T00:05:14Z","timestamp":1726358714000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-29959-0_17"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019]]},"ISBN":["9783030299583","9783030299590"],"references-count":31,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-29959-0_17","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2019]]},"assertion":[{"value":"15 September 2019","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"ESORICS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"European Symposium on Research in Computer Security","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Luxembourg","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Luxembourg","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2019","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"23 September 2019","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27 September 2019","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"24","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"esorics2019","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/conf.laas.fr\/esorics\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"344","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"67","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"0","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"19% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3,2","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"11","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"This content has been made available to all.","name":"free","label":"Free to read"}]}}