More Web Proxy on the site http://driver.im/

Article

The case for analysis preserving language transformation

Authors:

Guillaume Marceau,

Liangzhao ZengAuthors Info & Claims

ISSTA '06: Proceedings of the 2006 international symposium on Software testing and analysis

Pages 191 - 202

https://doi.org/10.1145/1146238.1146260

Published: 21 July 2006 Publication History

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]

A. Aiken, M. Fahndrich, J. S. Foster, and Z. Su. A toolkit for constructing type- and constraint-based program analyses. In Types in Compilation, pages 78--96, 1998.

Digital Library

[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]

T. Ball and S. Rajamani. Automatically validating temporal safety properties of interfaces. In SPIN 2001 Workshop on Model Checking of Software, May 2001.

Digital Library

[7]

T. Ball and S. Rajamani. The slam project: Debugging system software via static analysis. In Proceedings of the 29th ACM Symposium on Principles of Programming Languages (POPL02), January 2002.

Digital Library

[8]

R. M. Balzer, N. M. Goldman, and D. S. Wile. On the Transformational Implementation Approach to Programming. In Proceedings of the 2nd International Conference on Software Engineering, pages 337--344, Oct. 1986.

Digital Library

[9]

I. D. Baxter, C. Pidgeon, and M. Mehlich. DMS: Program Transformations for Practical Scalable Software Evolution. In Proceedings of the 26th International Conference on Software Engineering, pages 625--634, May 2004.

Digital Library

[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]

H. Chen and D. Wagner. MOPS: An Infrastructure for Examining Security Properties of Software. In Proceedings of the 9th ACM Conference on Computer and Communications Security, pages 235--244, 2002.

Digital Library

[13]

P. Cousot. Abstract interpretation based static analysis parameterized by semantics. In SAS '97: Proceedings of the 4th International Symposium on Static Analysis, pages 388--394, London, UK, 1997. Springer-Verlag.

Digital Library

[14]

M. Das, S. Lerner, and M. Seigle. ESP: Pathsensitive program verification in polynomial time. In ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI '02), June 2002.

Digital Library

[15]

P. T. Devanbu. GENOA: A customizable languageand front-end independent code analyzer. In International Conference on Software Engineering, pages 307--317, 1992.

Digital Library

[16]

D. M. Doolin, J. Dongarra, and K. Seymour. JLAPACK - Compiling LAPACK Fortran to Java. Technical report, University of Tennessy, June 1998. Available at http://www.cs.utk.edu/ library/TechReports/1998/utcs- 98--390.ps.Z.

Digital Library

[17]

T. Eisenbarth, R. Koschke, and D. Simon. Aiding program comprehension by static and dynamic feature analysis. In ICSM, pages 602--611, 2001.

Digital Library

[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.

Digital Library

[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.

Digital Library

[21]

J. Foster, M. Fahndrich, and A. Aiken. A theory of type qualifiers. In ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI '99), pages 192--203, May 1999.

Digital Library

[22]

J. Foster, T. Terauchi, and A. Aiken. Flow-Sensitive Type Qualifiers. In ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI '02), 2002.

Digital Library

[23]

V. Ganapathy, S. Jha, D. Chandler, D. Melski, and D. Vitek. Buffer overrun detection using linear programming and static analysis. In Proceedings of the 10th ACM Conference on Computer and Communications Security, pages 345--354, Washington, DC, 2003.

Digital Library

[24]

S. Hallem, B. Chelf, Y. Xie, and D. Engler. A system and language for building system-specific static analyses. In ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI '02), June 2002.

Digital Library

[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.

Digital Library

[30]

L. Koved, M. Pistoia, and A. Kershenbaum. Access rights analysis for java. In Proceedings of the 17th Annual ACM Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA 2002), pages 359--372, November 2002.

Digital Library

[31]

D. Larochelle and D. Evans. Statically detecting likely buffer overflow vulnerabilities. In Proceedings of the Tenth USENIX Security Symposium, pages 177--190, 2001.

Digital Library

[32]

C. Lattner and V. Adve. LLVM: A Compilation Framework for Lifelong Program Analysis & Transformation. In Proceedings of the 2004 International Symposium on Code Generation and Optimization (CGO'04), Palo Alto, California, Mar 2004.

Digital Library

[33]

J. Martin. Ephedra - a c to java migration environment, April 2002. Ph.D. Dissertation, University of Victoria, Kanada. Available at http://ovid.tigris.org/Ephedra/.

Digital Library

[34]

J. Morgenthaler. Static Analysis for a Software Transformation Tool. PhD thesis, 1997.

Digital Library

[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.

Digital Library

[39]

A. Rountev, A. Milanova, and B. G. Ryder. Points-to analysis for java using annotated constraints. In Conference on Object-Oriented, pages 43--55, 2001.

Digital Library

[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.

Digital Library

[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.

Digital Library

[43]

R. E. Strom and D. M. Yellin. Extending typestate checking using conditional liveness analysis. IEEE Transactions on Software Engineering, 19(5):478--485, May 1993.

Digital Library

[44]

R. E. Strom and S. Yemini. Typestate: A programming language concept for enhancing software reliability. IEEE Transactions on Software Engineering, 12(1):157--171, Jan. 1986.

Digital Library

[45]

M. M. Strout, J. Mellor-Crummey, and P. Hovland. Representation-independent program analysis. In Proceedings of the The sixth ACM SIGPLAN-SIGSOFT Workshop on Program Analysis for Software Tools and Engineering (PASTE), September 5-6 2005.

Digital Library

[46]

A. von Mayrhauser and S. Lang. On the role of static analysis during software maintenance. In Proceedings of International Workshop on Program Comprehension, pages 170--177, 1999.

Digital Library

[47]

C. Wright, C. Cowan, J. Morris, S. Smalley, and G. Kroah-Hartman. Linux security modules: General security support for the linux kernel. In Proceedings of the 11th USENIX Security Symposium, 2002.

Digital Library

[48]

E. Yahav and G. Ramalingam. Verifying safety properties using separation and heterogeneous abstractions. In PLDI '04: Proceedings of the ACM SIGPLAN 2004 conference on Programming language design and implementation, pages 25--34, New York, NY, USA, 2004. ACM Press.

Digital Library

[49]

X. Zhang, A. Edwards, and T. Jaeger. Using cqual for static analysis of authorization hook placement. In Proceedings of the 11th USENIX Security Symposium, 2002.

Digital Library

[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.

Cited By

Zhang BChen WYao PWang CTang WZhang CTsafrir DMusuvathi MGupta RAbu-Ghazaleh N(2024)SIRO: Empowering Version Compatibility in Intermediate Representations via Program SynthesisProceedings of the 29th ACM International Conference on Architectural Support for Programming Languages and Operating Systems, Volume 310.1145/3620666.3651366(882-899)Online publication date: 27-Apr-2024
https://dl.acm.org/doi/10.1145/3620666.3651366
Grimmer AAngerer FPrahofer HGrunbacher P(2016)Supporting Program Analysis for Non-Mainstream Languages: Experiences and Lessons Learned2016 IEEE 23rd International Conference on Software Analysis, Evolution, and Reengineering (SANER)10.1109/SANER.2016.15(460-469)Online publication date: Mar-2016
https://doi.org/10.1109/SANER.2016.15
Li JPombrio JPolitz JKrishnamurthi SMurphy GJr. G(2015)Slimming languages by reducing sugar: a case for semantics-altering transformations2015 ACM International Symposium on New Ideas, New Paradigms, and Reflections on Programming and Software (Onward!)10.1145/2814228.2814240(90-106)Online publication date: 21-Oct-2015
https://dl.acm.org/doi/10.1145/2814228.2814240
Show More Cited By

Index Terms

The case for analysis preserving language transformation

Recommendations

Jeannie: granting java native interface developers their wishes
Proceedings of the 2007 OOPSLA conference

Higher-level languages interface with lower-level languages such as C to access platform functionality, reuse legacy libraries, or improve performance. This raises the issue of how to best integrate different languages while also reconciling ...
Jeannie: granting java native interface developers their wishes
OOPSLA '07: Proceedings of the 22nd annual ACM SIGPLAN conference on Object-oriented programming systems, languages and applications

Higher-level languages interface with lower-level languages such as C to access platform functionality, reuse legacy libraries, or improve performance. This raises the issue of how to best integrate different languages while also reconciling ...
A Value Analysis for C Programs
SCAM '09: Proceedings of the 2009 Ninth IEEE International Working Conference on Source Code Analysis and Manipulation

We demonstrate the value analysis of Frama-C. Frama-C is an Open Source static analysis framework for the C language. In Frama-C, each static analysis technique, approach or idea can be implemented as a new plug-in, with the opportunity to obtain ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

ISSTA '06: Proceedings of the 2006 international symposium on Software testing and analysis

July 2006

274 pages

ISBN:1595932631

DOI:10.1145/1146238

General Chair:
Lori Pollock
University of Delaware, USA
,
Program Chair:
Mauro Pezzè
Università degli Studi di Milano Bicocca, Italy

Copyright © 2006 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Sponsors

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 21 July 2006

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Article

Conference

ISSTA06

Sponsor:

ISSTA06: International Symposium on Software Testing and Analysis 2006

July 17 - 20, 2006

Maine, Portland, USA

Acceptance Rates

Overall Acceptance Rate 58 of 213 submissions, 27%

Upcoming Conference

ISSTA '25

Sponsor:
sigsoft

34th ACM SIGSOFT International Symposium on Software Testing and Analysis

June 25 - 28, 2025

Trondheim , Norway

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

8
Total Citations
View Citations
390
Total Downloads

Downloads (Last 12 months)7
Downloads (Last 6 weeks)0

Reflects downloads up to 13 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

Zhang BChen WYao PWang CTang WZhang CTsafrir DMusuvathi MGupta RAbu-Ghazaleh N(2024)SIRO: Empowering Version Compatibility in Intermediate Representations via Program SynthesisProceedings of the 29th ACM International Conference on Architectural Support for Programming Languages and Operating Systems, Volume 310.1145/3620666.3651366(882-899)Online publication date: 27-Apr-2024
https://dl.acm.org/doi/10.1145/3620666.3651366
Grimmer AAngerer FPrahofer HGrunbacher P(2016)Supporting Program Analysis for Non-Mainstream Languages: Experiences and Lessons Learned2016 IEEE 23rd International Conference on Software Analysis, Evolution, and Reengineering (SANER)10.1109/SANER.2016.15(460-469)Online publication date: Mar-2016
https://doi.org/10.1109/SANER.2016.15
Li JPombrio JPolitz JKrishnamurthi SMurphy GJr. G(2015)Slimming languages by reducing sugar: a case for semantics-altering transformations2015 ACM International Symposium on New Ideas, New Paradigms, and Reflections on Programming and Software (Onward!)10.1145/2814228.2814240(90-106)Online publication date: 21-Oct-2015
https://dl.acm.org/doi/10.1145/2814228.2814240
Nadera BChitraprasad DChandra V(2012)The varying faces of a program transformation systemsACM Inroads10.1145/2077808.20778253:1(49-55)Online publication date: 1-Mar-2012
https://dl.acm.org/doi/10.1145/2077808.2077825
Sridharan MArtzi SPistoia MGuarnieri STripp OBerg R(2011)F4FACM SIGPLAN Notices10.1145/2076021.204814546:10(1053-1068)Online publication date: 22-Oct-2011
https://dl.acm.org/doi/10.1145/2076021.2048145
Sridharan MArtzi SPistoia MGuarnieri STripp OBerg RLopes CFisher K(2011)F4FProceedings of the 2011 ACM international conference on Object oriented programming systems languages and applications10.1145/2048066.2048145(1053-1068)Online publication date: 22-Oct-2011
https://dl.acm.org/doi/10.1145/2048066.2048145
Centonze PFlynn RPistoia M(2007)Combining Static and Dynamic Analysis for Automatic Identification of Precise Access-Control PoliciesTwenty-Third Annual Computer Security Applications Conference (ACSAC 2007)10.1109/ACSAC.2007.39(292-303)Online publication date: Dec-2007
https://doi.org/10.1109/ACSAC.2007.39
Centonze PNaumovich GFink SPistoia MPollock LPezzè M(2006)Role-Based access control consistency validationProceedings of the 2006 international symposium on Software testing and analysis10.1145/1146238.1146253(121-132)Online publication date: 21-Jul-2006
https://dl.acm.org/doi/10.1145/1146238.1146253

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Table of Contents