The case for analysis preserving language transformation

ABSTRACT

Static analysis has gained much attention over the past few years in applications such as bug finding and program verification. As software becomes more complex and componentized, it is common for software systems and applications to be implemented in multiple languages. There is thus a strong need for developing analysis tools for multi-language software. We introduce a technique called Analysis Preserving Language Transformation (aplt) that enables the analysis of multi-language software, and also allows analysis tools for one language to be applied to programs written in another. aplt preserves data and control flow information needed to perform static analyses, but allows the translation to deviate from the original program's semantics in ways that are not pertinent to the particular analysis. We discuss major technical difficulties in building such a translator, using a C-to-Java translator as an example. We demonstrate the feasibility and effectiveness of aplt using two usage cases: analysis of the Java runtime native methods and reuse of Java analysis tools for C. Our preliminary results show that a control- and data-flow equivalent model for native methods can eliminate unsoundness and produce reliable results, and that aplt enables seamless reuse of analysis tools for checking high-level program properties.

REFERENCES

• 1: Security Focus Bugtraq Posting. http://cert.unistuttgart.de/archive/bugtraq/2001/03/msg00420.html.
• 2: The SUIF 2 Compiler System. Available at http://suif.stanford.edu/suif/suif2/index.html.
• 3: The vortex project. Available at http://www.cs.washington.edu/research/projects/cecil/www/vortex.html.
• 4: Alexander Aiken , Manuel Fähndrich , Jeffrey S. Foster , Zhendong Su, A Toolkit for Constructing Type- and Constraint-Based Program Analyses, Proceedings of the Second International Workshop on Types in Compilation, p.78-96, March 25-27, 1998
• 5: American National Standards Institute, 1430 Broadway, New York, NY 10018, USA. ANSI Fortran X3.9-1978, 1978. Approved April 3, 1978 (also known as Fortran 77).
• 6: Thomas Ball , Sriram K. Rajamani, Automatically validating temporal safety properties of interfaces, Proceedings of the 8th international SPIN workshop on Model checking of software, p.103-122, May 2001, Toronto, Ontario, Canada
• 7: Thomas Ball , Sriram K. Rajamani, The SLAM project: debugging system software via static analysis, Proceedings of the 29th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.1-3, January 16-18, 2002, Portland, Oregon
• 8: Robert Balzer , Neil Goldman , David Wile, On the Transformational Implementation approach to programming, Proceedings of the 2nd international conference on Software engineering, p.337-344, October 13-15, 1976, San Francisco, California, United States
• 9: Ira D. Baxter , Christopher Pidgeon , Michael Mehlich, DMS®: Program Transformations for Practical Scalable Software Evolution, Proceedings of the 26th International Conference on Software Engineering, p.625-634, May 23-28, 2004
• 10: M. Bishop and M. Dilger. Checking for race conditions in file accesses. Computing Systems, 9(2):131--152, 1996.
• 11: H. Chen, D. Dean, and D. Wagner. Model Checking One Million Lines of C Code. In Proceedings of the 11th Annual Network and Distributed System Security Symposium, San Diego, CA, Feb. 4-6, 2004.
• 12: Hao Chen , David Wagner, MOPS: an infrastructure for examining security properties of software, Proceedings of the 9th ACM conference on Computer and communications security, November 18-22, 2002, Washington, DC, USA [doi>10.1145/586110.586142]
• 13: Patrick Cousot, Abstract Interpretation Based Static Analysis Parameterized by Semantics, Proceedings of the 4th International Symposium on Static Analysis, p.388-394, September 08-10, 1997
• 14: Manuvir Das , Sorin Lerner , Mark Seigle, ESP: path-sensitive program verification in polynomial time, Proceedings of the ACM SIGPLAN 2002 Conference on Programming language design and implementation, June 17-19, 2002, Berlin, Germany
• 15: Premkumar T. Devanbu, GENOA: a customizable language- and front-end independent code analyzer, Proceedings of the 14th international conference on Software engineering, p.307-317, May 11-15, 1992, Melbourne, Australia [doi>10.1145/143062.143148]
• 16: David Doolin , Jack Dongarra , Keith Seymour, JLAPACK -- Compiling LAPACK Fortran to Java, University of Tennessee, Knoxville, TN, 1998
• 17: Aiding Program Comprehension by Static and Dynamic Feature Analysis, Proceedings of the IEEE International Conference on Software Maintenance (ICSM'01), p.602, November 07-09, 2001
• 18: D. Engler, B. Chelf, A. Chou, and S. Hallem. Checking system rules using system-specific, programmer-written compiler extensions. In Proceedings of the Fourth Symposium on Operation System Design and Implementation (OSDI), October 2000.
• 19: A. M. Erosa and L. J. Hendren. Taming Control Flow:A Structured Approach to Eliminating Goto Statements. In Proceedings of the 1994 InternationalConference on Computer Languages, pages 229--240, May 16-19, 1994. Toulouse, France.
• 20: J. Field, D. Goyal, G. Ramalingam, and E. Yahav. Typestate verification: Abstraction techniques and complexity results, 2003.
• 21: Jeffrey S. Foster , Manuel Fähndrich , Alexander Aiken, A theory of type qualifiers, Proceedings of the ACM SIGPLAN 1999 conference on Programming language design and implementation, p.192-203, May 01-04, 1999, Atlanta, Georgia, United States
• 22: Jeffrey S. Foster , Tachio Terauchi , Alex Aiken, Flow-sensitive type qualifiers, Proceedings of the ACM SIGPLAN 2002 Conference on Programming language design and implementation, June 17-19, 2002, Berlin, Germany
• 23: Vinod Ganapathy , Somesh Jha , David Chandler , David Melski , David Vitek, Buffer overrun detection using linear programming and static analysis, Proceedings of the 10th ACM conference on Computer and communications security, October 27-30, 2003, Washington D.C., USA [doi>10.1145/948109.948155]
• 24: Seth Hallem , Benjamin Chelf , Yichen Xie , Dawson Engler, A system and language for building system-specific, static analyses, Proceedings of the ACM SIGPLAN 2002 Conference on Programming language design and implementation, June 17-19, 2002, Berlin, Germany
• 25: IBM. The toronto portable optimizer.
• 26: S. K. Jain, G. Marceau, X. Zhang, L. Koved, and T. Jaeger. INTELLECT: INTErmediate-Language LEvel C Translator. Technical Report 23907, IBM, 2006. Available at http://domino.research.ibm.com/library/cyberdig.nsf/index.html.
• 27: Jazillian, Inc. How to convert c to java. Available at http://jazillian.com/how.html.
• 28: T. Jensen, D. Metayer, and T. Thorn. Verification of control flow based security properties. In Proceedings of the 1999 IEEE Symposium on Security and Privacy, May 1999.
• 29: R. Johnson and D. Wagner. Finding user/kernel pointer bugs with type inference. In Proceedings of the USENIX Security Symposium, Aug. 2004.
• 30: Larry Koved , Marco Pistoia , Aaron Kershenbaum, Access rights analysis for Java, Proceedings of the 17th ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications, November 04-08, 2002, Seattle, Washington, USA
• 31: D. Larochelle and D. Evans. Statically detecting likely buffer overflow vulnerabilities. In Proceedings of the Tenth USENIX Security Symposium, pages 177--190, 2001.
• 32: Chris Lattner , Vikram Adve, LLVM: A Compilation Framework for Lifelong Program Analysis & Transformation, Proceedings of the international symposium on Code generation and optimization: feedback-directed and runtime optimization, p.75, March 20-24, 2004, Palo Alto, California
• 33: Johannes Martin , Hausi A. Muller, Ephedra: a c to java migration environment, 2002
• 34: John David Morgenthaler, Static analysis for a software transformation tool, University of California at San Diego, La Jolla, CA, 1998
• 35: N. Nethercote and J. Seward. Valgrind: A program supervision framework. In Proceedings of the Third Workshop on Runtime Verification (RV'03), Boulder, Colorado, USA, July 2003.
• 36: Novosoft. C to java converter. Available at http://in.tech.yahoo.com/020513/94/1nxuw.html.
• 37: R. W. O'Callahan. The shrike toolkit. Available at http://org.eclipse.cme/contributions/shrike/.
• 38: M. Pistoia, R. J. Flynn, L. Koved, and V. C. Sreedhar. Interprocedural analysis for privileged code placement and tainted variable detection. In ECOOP 2005 - Object-Oriented Programming: 19th European Conference, Glasgow, UK, July 25-29, 2005. Proceedings, volume 3586 of Lecture Notes in Computer Science, pages 362-386. Springer, Aug. 2005.
• 39: Atanas Rountev , Ana Milanova , Barbara G. Ryder, Points-to analysis for Java using annotated constraints, Proceedings of the 16th ACM SIGPLAN conference on Object oriented programming, systems, languages, and applications, p.43-55, October 14-18, 2001, Tampa Bay, FL, USA
• 40: B. G. Ryder. Dimensions of Precision in Reference Analysis of Object-Oriented Languages. In Proceedings of the 12th International Conference on Compiler Construction, pages 126--137, Warsaw, Poland, April 2003. Invited Paper.
• 41: J. H. Saltzer and M. D. Schroeder. The Protection of Information in Computer Systems. In Proceedings of the IEEE, volume 63, pages 1278--1308, Sept. 1975.
• 42: U. Shankar, K. Talwar, J. S. Foster, and D. Wagner. Detecting format string vulnerabilities with type qualifiers. In Proceedings of the Tenth USENIX Security Symposium, pages 201--216, 2001.
• 43: R. E. Strom , D. M. Yellin, Extending Typestate Checking Using Conditional Liveness Analysis, IEEE Transactions on Software Engineering, v.19 n.5, p.478-485, May 1993 [doi>10.1109/32.232013]
• 44: R E Strom , S Yemini, Typestate: A programming language concept for enhancing software reliability, IEEE Transactions on Software Engineering, v.12 n.1, p.157-171, Jan. 1986
• 45: Michelle Mills Strout , John Mellor-Crummey , Paul Hovland, Representation-independent program analysis, The 6th ACM SIGPLAN-SIGSOFT workshop on Program analysis for software tools and engineering, September 05-06, 2005, Lisbon, Portugal
• 46: Anneliese von Mayrhauser , Steve Lang, On the Role of Static Analysis during Software Maintenance, Proceedings of the 7th International Workshop on Program Comprehension, p.170, May 05-07, 1999
• 47: Chris Wright , Crispin Cowan , Stephen Smalley , James Morris , Greg Kroah-Hartman, Linux Security Modules: General Security Support for the Linux Kernel, Proceedings of the 11th USENIX Security Symposium, p.17-31, August 05-09, 2002
• 48: Eran Yahav , G. Ramalingam, Verifying safety properties using separation and heterogeneous abstractions, Proceedings of the ACM SIGPLAN 2004 conference on Programming language design and implementation, June 09-11, 2004, Washington DC, USA
• 49: Xiaolan Zhang , Antony Edwards , Trent Jaeger, Using CQUAL for Static Analysis of Authorization Hook Placement, Proceedings of the 11th USENIX Security Symposium, p.33-48, August 05-09, 2002
• 50: X. Zhang, T. Jaegert, and L. Koved. Applying Static Analysis to Verifying Security Properties. In Proceedings of the 2004 Grace Hopper Celebration of Women in Computing Conference, Chicago, IL, 2004. Also available as IBM technical report RC23246 at http://domino.research.ibm.com/library/cyberdig.nsf/index.html.

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.3 Coding Tools and Techniques

General Terms:
Languages, Security, Verification

Keywords:
C, Java, language transformation, language translation, security, static analysis, verification