Abstract
Modern software systems are not only famous for being ubiquitous and large scale but also infamous for being inherently insecure. We argue that a large part of this problem is due to the fact that current programming languages do not provide adequate built-in support for addressing security concerns.
In this work we outline the challenges involved in developing Codana, a novel programming language for defining provably correct dynamic analyses. Codana analyses form security monitors; they allow programmers to proactively protect their programs from security threats such as insecure information flows, buffer overflows and access-control violations. We plan to design Codana in such a way that program analyses will be simple to write, read and prove correct, easy to maintain and reuse, efficient to compile, easy to parallelize, and maximally amenable to static optimizations. This is difficult as, nevertheless, Codana must comprise sufficiently expressive language constructs to cover a large class of security-relevant dynamic analyses.
For deployed programs, we envision Codana-based analyses to be the last line of defense against malicious attacks. It is hence paramount to provide correctness guarantees on Codana-based analyses as well as the related program instrumentation and static optimizations.
A further challenge is effective but provably correct sharing: dynamic analyses can benefit from sharing information among another. We plan to encapsulate such shared information within Codana program fragments.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Chrome Browser, https://www.google.com/chrome
Safari Browser, http://www.apple.com/safari/
The WebKit Open-Source Project, http://www.webkit.org/
Aderhold, M., Cuéllar, J., Mantel, H., Sudbrock, H.: Exemplary formalization of secure coding guidelines. Technical Report TUD-CS-2010-0060, TU Darmstadt, Germany (2010)
Aktug, I., Gurov, D., Piessens, F., Seehusen, F., Vanoverberghe, D., Vétillard, E.: Static analysis algorithms and tools for code-contract compliance, Public Deliverable D3.1.2, S3MS (2006), http://s3ms.org
Aktug, I., Naliuka, K.: ConSpec–a formal language for policy specification. Electronic Notes in Theoretical Computer Science 197(1), 45–58 (2008)
Ansaloni, D., Binder, W., Bockisch, C., Bodden, E., Hatun, K., Marek, L., Qi, Z., Sarimbekov, A., Sewe, A., Tůma, P., Zheng, Y.: Challenges for Refinement and Composition of Instrumentations: Position Paper. In: Gschwind, T., De Paoli, F., Gruhn, V., Book, M. (eds.) SC 2012. LNCS, vol. 7306, pp. 86–96. Springer, Heidelberg (2012)
The Aspect J. home page (2003)
Austin, T.H., Flanagan, C.: Efficient purely-dynamic information flow analysis. In: Proceedings of the ACM SIGPLAN Fourth Workshop on Programming Languages and Analysis for Security, PLAS 2009, pp. 113–124. ACM, New York (2009)
Avgustinov, P., Christensen, A.S., Hendren, L., Kuzins, S., Lhoták, J., Lhoták, O., de Moor, O., Sereni, D., Sittampalam, G., Tibble, J.: Abc: an extensible aspectj compiler. In: Proceedings of the 4th International Conference on Aspect-Oriented Software Development, AOSD 2005, pp. 87–98. ACM, New York (2005)
Barnett, M., Leino, K., Schulte, W.: The spec# programming system: An overview. Construction and analysis of safe, secure, and interoperable smart devices, 49–69 (2005)
Bisht, P., Venkatakrishnan, V.: Xss-guard: precise dynamic prevention of cross-site scripting attacks. Detection of Intrusions and Malware, and Vulnerability Assessment, 23–43 (2008)
Bodden, E.: Verifying finite-state properties of large-scale programs. PhD thesis, McGill University, Available in print through ProQuest (June 2009)
Bodden, E.: Efficient hybrid typestate analysis by determining continuation-equivalent states. In: Proceedings of the 32nd ACM/IEEE International Conference on Software Engineering ICSE 2010, vol. 1, pp. 5–14. ACM, New York (2010)
Bodden, E.: Continuation equivalence: a correctness criterion for static optimizations of dynamic analyses. In: WODA 2011: International Workshop on Dynamic Analysis, pp. 24–28. ACM (July 2011)
Bodden, E., Havelund, K.: Racer: Effective race detection using AspectJ. In: International Symposium on Software Testing and Analysis (ISSTA 2008), Seattle, WA, pp. 155–165. ACM, New York (2008)
Bodden, E., Havelund, K.: Aspect-oriented race detection in Java. IEEE Transactions on Software Engineering (TSE) 36(4), 509–527 (2010)
Bodden, E., Hendren, L.: The Clara framework for hybrid typestate analysis. International Journal on Software Tools for Technology Transfer (STTT), 1–20 (2010)
Bodden, E., Hendren, L., Lhoták, O.: A Staged Static Program Analysis to Improve the Performance of Runtime Monitoring. In: Bateni, M. (ed.) ECOOP 2007. LNCS, vol. 4609, pp. 525–549. Springer, Heidelberg (2007)
Bodden, E., Lam, P., Hendren, L.: Finding programming errors earlier by evaluating runtime monitors ahead-of-time. In: 16th ACM SIGSOFT International Symposium on Foundations of Software Engineering (SIGSOFT 2008/FSE-16), pp. 36–47. ACM, New York (2008)
Bodden, E., Lam, P., Hendren, L.: Clara: A Framework for Partially Evaluating Finite-State Runtime Monitors Ahead of Time. In: Barringer, H., Falcone, Y., Finkbeiner, B., Havelund, K., Lee, I., Pace, G., Roşu, G., Sokolsky, O., Tillmann, N. (eds.) RV 2010. LNCS, vol. 6418, pp. 183–197. Springer, Heidelberg (2010)
Dwyer, M.B., Purandare, R.: Residual dynamic typestate analysis exploiting static analysis: results to reformulate and reduce the cost of dynamic analysis. In: Proceedings of the Twenty-Second IEEE/ACM International Conference on Automated Software Engineering, ASE 2007, pp. 124–133. ACM, New York (2007)
Erlingsson, U.: The inlined reference monitor approach to security policy enforcement. PhD thesis, Cornell University (2003)
Inostroza, M., Tanter, É., Bodden, E.: Modular reasoning with join point interfaces. Technical Report TUD-CS-2011-0272, CASED (October 2011)
Inostroza, M., Tanter, E., Bodden, E.: Join point interfaces for modular reasoning in aspect-oriented programs. In: ESEC/FSE 2011: Joint Meeting of the European Software Engineering Conference and the ACM SIGSOFT Symposium on the Foundations of Software Engineering, pp. 508–511 (2011)
Jones, R.W.M., Kelly, P.H.J.: Backwards-compatible bounds checking for arrays and pointers in C programs. In: AADEBUG, pp. 13–26 (1997)
Kiczales, G., Lamping, J., Mendhekar, A., Maeda, C., Lopes, C., Loingtier, J., Irwin, J.: Aspect-Oriented Programming. In: Aksit, M., Auletta, V. (eds.) ECOOP 1997. LNCS, vol. 1241, pp. 220–242. Springer, Heidelberg (1997)
Le, W., Soffa, M.L.: Generating analyses for detecting faults in path segments. In: Proceedings of the 2011 International Symposium on Software Testing and Analysis, ISSTA 2011, pp. 320–330. ACM, New York (2011)
Marek, L., Villazón, A., Zheng, Y., Ansaloni, D., Binder, W., Qi, Z.: Disl: a domain-specific language for bytecode instrumentation. In: AOSD 2012, pp. 239–250. ACM, New York (2012)
Naeem, N.A., Lhotak, O.: Typestate-like analysis of multiple interacting objects. In: Proceedings of the 23rd ACM SIGPLAN Conference on Object-Oriented Programming Systems Languages and Applications, OOPSLA 2008, pp. 347–366. ACM, New York (2008)
Rodriguez, J., Lhoták, O.: Actor-Based Parallel Dataflow Analysis. In: Knoop, J. (ed.) CC 2011. LNCS, vol. 6601, pp. 179–197. Springer, Heidelberg (2011)
Ruwase, O., Lam, M.S.: A practical dynamic buffer overflow detector. In: Proceedings of the 11th Annual Network and Distributed System Security Symposium, pp. 159–169 (2004)
Schneider, F.: Enforceable security policies. ACM Transactions on Information and System Security (TISSEC) 3(1), 30–50 (2000)
Vogt, P., Nentwich, F., Jovanovic, N., Kirda, E., Kruegel, C., Vigna, G.: Cross-site scripting prevention with dynamic data tainting and static analysis. In: Proceeding of the Network and Distributed System Security Symposium (NDSS), vol. 42 (2007)
W3C. Same-Origin Policy, http://www.w3.org/Security/wiki/Same_Origin_Policy
Yong, S.H., Horwitz, S.: Using static analysis to reduce dynamic analysis overhead. Form. Methods Syst. Des. 27(3), 313–334 (2005)
Zee, K., Kuncak, V., Rinard, M.: Full functional verification of linked data structures. In: PLDI 2008, pp. 349–361. ACM, New York (2008)
Zhivich, M., Leek, T., Lippmann, R.: Dynamic buffer overflow detection. In: Workshop on the Evaluation of Software Defect Detection Tools (2005)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2012 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Bodden, E., Follner, A., Rasthofer, S. (2012). Challenges in Defining a Programming Language for Provably Correct Dynamic Analyses. In: Margaria, T., Steffen, B. (eds) Leveraging Applications of Formal Methods, Verification and Validation. Technologies for Mastering Change. ISoLA 2012. Lecture Notes in Computer Science, vol 7609. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-34026-0_2
Download citation
DOI: https://doi.org/10.1007/978-3-642-34026-0_2
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-34025-3
Online ISBN: 978-3-642-34026-0
eBook Packages: Computer ScienceComputer Science (R0)