article

A framework for the static verification of api calls

Authors:

Diomidis Spinellis,

Panagiotis LouridasAuthors Info & Claims

Journal of Systems and Software, Volume 80, Issue 7

Pages 1156 - 1168

https://doi.org/10.1016/j.jss.2006.09.040

Published: 01 July 2007 Publication History

Abstract

A number of tools can statically check program code to identify commonly encountered bug patterns. At the same time, programs are increasingly relying on external apis for performing the bulk of their work: the bug-prone program logic is being fleshed-out, and many errors involve tricky subroutine calls to the constantly growing set of external libraries. Extending the static analysis tools to cover the available apis is an approach that replicates scarce human effort across different tools and does not scale. Instead, we propose moving the static api call verification code into the api implementation, and distributing the verification code together with the library proper. We have designed a framework for providing static verification code together with Java classes, and have extended the FindBugs static analysis tool to check the corresponding method invocations. To validate our approach we wrote verification tests for 100 different methods, and ran FindBugs on 6.9 million method invocations on what amounts to about 13 million lines of production-quality code. In the set of 55 thousand method invocations that could potentially be statically verified our approach identified 800 probable errors.

References

[1]

The Java Programming Language. fourth ed. Addison-Wesley, Boston, MA.

[2]

Combining test case generation and runtime verification. Theor. Comput. Sci. v336 i2-3. 209-234.

Digital Library

[3]

Ball, T., Rajamani, S.K., 2002. The SLAM project: debugging system software via static analysis. In: POPL'02: Proceedings of the 29th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 1-3.

Digital Library

[4]

Ball, T., Cook, B., Levin, V., Rajamani, S.K., 2004. SLAM and static driver verifier: technology transfer of formal methods inside Microsoft. Tech. Rep. MSR-TR-2004-08, Microsoft Research, Redmond, WA.

[5]

A technique for finding storage allocation errors in C-language programs. SIGPLAN Notices. v17 i7. 32-38.

Digital Library

[6]

Barringer, H., Finkbeiner, B., Gurevich, Y., Sipma, H.B. (Eds.), 2006. Proceedings of the Fifth Workshop on Runtime Verification (RV 2005). Electronic Notes in Theoretical Computer Science, 144(4).

[7]

Test infected: programmers love writing tests. Java Report. v3 i7. 37-50.

[8]

Blanchet, B., Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Miné, A., Monniaux, D., Rival, X., 2003. A static analyzer for large safety-critical software. In: PLDI'03: Proceedings of the ACM SIGPLAN 2003 Conference on Programming Language Design and Implementation, pp. 196-207.

Digital Library

[9]

An overview of JML tools and applications. Int. J. Software Tools Technol. Transfer. v7 i3. 212-232.

[10]

A static analyzer for finding dynamic programming errors. Software-Pract. Exp. v30 i7. 775-802.

Digital Library

[11]

Chaki, S., Clarke, E., Groce, A., Jha, S., Veith, H., 2003. Modular verification of software components in C. In: ICSE'03: Proceedings of the 25th International Conference on Software Engineering, pp. 385-395.

Digital Library

[12]

Chen, H., Wagner, D., 2002. MOPS: an infrastructure for examining security properties of software. In: CCS'02: Proceedings of the 9th ACM Conference on Computer and Communications Security, pp. 235-244.

Digital Library

[13]

ESC/Java2: Uniting ESC/Java and JML-progress and issues in building and using ESC/Java2. In: Barthe, G., Burdy, L., Huisman, M. (Eds.), Lecture Notes in Computer Science, vol. 3362. Springer-Verlag. pp. 108-129.

[14]

PMD Applied. Centennial Books.

[15]

Corbett, J.C., Dwyer, M.B., Hatcliff, J., Laubach, S., Pasareanu, C.S., Robby, Zheng, H., 2000. Bandera: extracting finite-state models from Java source code. In: ICSE'00: Proceedings of the 22nd International Conference on Software engineering, pp. 439-448.

Digital Library

[16]

Cousot, P., Cousot, R., 1977. Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: POPL'77: Proceedings of the 4th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, pp. 238-252.

Digital Library

[17]

Csallner, C., Smaragdakis, Y., 2005. Check 'n' crash: Combining static checking and testing. In: ICSE'05: Proceedings of the 27th International Conference on Software Engineering, pp. 422-431.

Digital Library

[18]

Byte code engineering. In: Cap, C.H. (Ed.), JIT'99, Java-Informations-Tage 1999, Springer-Verlag. pp. 267-277.

[19]

Das, M., Lerner, S., Seigle, M., 2002. ESP: Path-sensitive program verification in polynomial time. In: PLDI'02: Proceedings of the ACM SIGPLAN 2002 Conference on Programming Language Design and Implementation, pp. 57-68.

Digital Library

[20]

DeLine, R., Fähndrich, M., 2001. Enforcing high-level protocols in low-level software. In: PLDI'01: Proceedings of the ACM SIGPLAN 2001 Conference on Programming Language Design and Implementation, pp. 59-69.

Digital Library

[21]

DeLine, R., Fähndrich, M., 2004. The Fugue protocol checker: Is your software Baroque? Tech. Rep. MSR-TR-2004-07, Microsoft Research, Redmond, WA.

[22]

Engler, D., Chen, D.Y., Hallem, S., Chou, A., Chelf, B., 2001. Bugs as deviant behavior: A general approach to inferring errors in systems code. In: SOSP'01: Proceedings of the Eighteenth ACM Symposium on Operating Systems Principles, pp. 57-72.

Digital Library

[23]

Improving security using extensible lightweight static analysis. IEEE Software. v19 i1. 42-51.

Digital Library

[24]

Design and code inspections to reduce errors in program development. IBM Syst. J. v15 i3. 182-211.

[25]

DrScheme: a programming environment for Scheme. J. Funct. Program. v12 i2. 159-182.

Digital Library

[26]

Flanagan, C., Leino, K.R.M., 2001. Houdini, an annotation assistant for ESC/Java. In: FME'01: Proceedings of the International Symposium of Formal Methods Europe on Formal Methods for Increasing Software Productivity, pp. 500-517.

Digital Library

[27]

Flanagan, C., Leino, K.R.M., Lillibridge, M., Nelson, G., Saxe, J.B., Stata, R., 2002. Extended static checking for Java. In: PLDI'02: Proceedings of the ACM SIGPLAN 2002 Conference on Programming Language Design and Implementation, pp. 234-245.

Digital Library

[28]

In: Guttag, J.V., Horning, J.J. (Eds.), Larch: Languages and Tools for Formal Specification, Springer-Verlag.

Digital Library

[29]

Hallem, S., Chelf, B., Xie, Y., Engler, D., 2002. A system and language for building system-specific, static analyses. In: PLDI'02: Proceedings of the ACM SIGPLAN 2002 Conference on Programming Language Design and Implementation, pp. 69-82.

Digital Library

[30]

An overview of the runtime verification tool Java PathExplorer. Formal Methods Syst. Design. v24 i2. 189-215.

Digital Library

[31]

Hovemeyer, D., Pugh, W., 2004. Finding bugs is easy. In: OOPSLA'04: Companion to the 19th Annual ACM SIGPLAN Conference on Object-Oriented Programming Systems, Languages, and Applications, pp. 132-136.

Digital Library

[32]

Aspect: detecting bugs with abstract dependences. ACM Trans. Software Eng. Methodol. v4 i2. 109-145.

Digital Library

[33]

Jim, T., Morrisett, G., Grossman, D., Hicks, M., Cheney, J., Wang, Y., 2002. Cyclone: a safe dialect of C. In: USENIX Annual Technical Conference, pp. 275-288.

Digital Library

[34]

JLint, 2004. JLint. Available online <http://jlint.sourceforge.net/>.

[35]

Johnson, S., 1977. Lint, a C program checker. Computer Science Technical Report 65, Bell Laboratories, Murray Hill, NJ.

[36]

Language development tools. Bell Syst. Technical J. v56 i6. 2155-2176.

[37]

Systematic Software Development using VDM. Prentice-Hall, Englewood Cliffs, NJ.

Digital Library

[38]

Getting started with ASPECTJ. Commun. ACM. v44 i10. 59-65.

Digital Library

[39]

Righting software. IEEE Software. v21 i3. 92-100.

[40]

Leavens, G.T., Baker, A.T., Ruby, C., 2005. Preliminary design of JML: A behavioral interface specification for Java. Tech. Rep. TR #98-06-rev28, Department of Computer Science, University of Iowa, Ames, IA.

[41]

Detecting software defects in telecom applications through lightweight static analysis: a war story. In: Lecture Notes in Computer Science, vol. 3302. Springer. pp. 91-106.

Digital Library

[42]

Mandelin, D., Xu, L., Bodí¿k, R., Kimelman, D., 2005. Jungloid mining: helping to navigate the api jungle. In: PLDI'05: Proceedings of the 2005 ACM SIGPLAN Conference on Programming Language Design and Implementation, pp. 48-61.

Digital Library

[43]

Marinov, D., Khurshid, S., 2001. TestEra: A novel framework for automated testing of Java programs. In: ASE'01: Proceedings of the 16th IEEE International Conference on Automated Software Engineering. IEEE Computer Society, Washington, DC, USA, p. 22.

Digital Library

[44]

Object-Oriented Software Construction. second ed. Prentice Hall PTR, Upper Saddle River, NJ.

Digital Library

[45]

Monitoring interfaces for faults. Electron. Notes Theor. Comput. Sci. v144 i4. 73-89.

[46]

Reimer, D., Schonberg, E., Srinivas, K., Srinivasan, H., Alpern, B., Johnson, R.D., Kershenbaum, A., Koved, L., 2004. SABER: Smart analysis based error reduction. In: ISSTA'04: Proceedings of the 2004 ACM SIGSOFT International Symposium on Software Testing and Analysis, pp. 243-251.

Digital Library

[47]

Rutar, N., Almazan, C.B., Foster, J.S., 2004. A comparison of bug finding tools for Java. In: ISSRE'04: Proceedings of the 15th International Symposium on Software Reliability Engineering (ISSRE'04), pp. 245-256.

Digital Library

[48]

Notable design patterns for domain specific languages. J. Syst. Software. v56 i1. 91-99.

Digital Library

[49]

Code Quality: The Open Source Perspective. Addison-Wesley, Boston, MA.

[50]

Component Software: Behind Object-Oriented Programming. second ed. Addison-Wesley, Reading, MA.

Digital Library

[51]

Viega, J., Bloch, J.T., Kohno, Y., McGraw, G., 2000. ITS4: A static vulnerability scanner for C and C++ code. In: ACSAC'00: Proceedings of the 16th Annual Computer Security Applications Conference, p. 257.

Digital Library

[52]

Weiser, M., 1981. Program slicing. In: ICSE'81: Proceedings of the 5th International Conference on Software Engineering, pp. 439-449.

Digital Library

[53]

A practical soft type system for Scheme. ACM Trans. Prog. Lang. Syst. v19 i1. 87-152.

Digital Library

Cited By

Kechagia MDevroey XPanichella AGousios Gvan Deursen AZhang DMøller A(2019)Effective and efficient API misuse detection via exception propagation and search-based testingProceedings of the 28th ACM SIGSOFT International Symposium on Software Testing and Analysis10.1145/3293882.3330552(192-203)Online publication date: 10-Jul-2019
https://dl.acm.org/doi/10.1145/3293882.3330552
Allen NKrishnan PScholz BMøller ANaik M(2015)Combining type-analysis with points-to analysis for analyzing Java library source-codeProceedings of the 4th ACM SIGPLAN International Workshop on State Of the Art in Program Analysis10.1145/2771284.2771287(13-18)Online publication date: 14-Jun-2015
https://dl.acm.org/doi/10.1145/2771284.2771287
Wang RZhou YChen SQadeer SEvans DGurevich YKing S(2013)Explicating SDKsProceedings of the 22nd USENIX conference on Security10.5555/2534766.2534801(399-414)Online publication date: 14-Aug-2013
https://dl.acm.org/doi/10.5555/2534766.2534801
Show More Cited By

Recommendations

Improving your software using static analysis to find bugs
OOPSLA '06: Companion to the 21st ACM SIGPLAN symposium on Object-oriented programming systems, languages, and applications

FindBugs looks for bugs in Java programs. It is based on the concept of bug patterns. A bug pattern is a code idiom that is often an error. Bug patterns arise for a variety of reasons, such as difficult language features, misunderstood API semantics, ...
API recommendation system for software development
ASE '16: Proceedings of the 31st IEEE/ACM International Conference on Automated Software Engineering

Nowadays, software developers often utilize existing third party libraries and make use of Application Programming Interface (API) to develop a software. However, it is not always obvious which library to use or whether the chosen library will play ...
Generating REST API Specifications through Static Analysis
ICSE '24: Proceedings of the IEEE/ACM 46th International Conference on Software Engineering

Web Application Programming Interfaces (APIs) allow services to be accessed over the network. RESTful (or REST) APIs, which use the REpresentation State Transfer (REST) protocol, are a popular type of web API. To use or test REST APIs, developers use ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Journal of Systems and Software

Journal of Systems and Software Volume 80, Issue 7

July, 2007

249 pages

ISSN:0164-1212

Issue’s Table of Contents

Copyright © Elsevier Inc. © 2006.

Publisher

Elsevier Science Inc.

United States

Publication History

Published: 01 July 2007

Author Tags

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

4
Total Citations
View Citations
0
Total Downloads

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

Reflects downloads up to 04 Sep 2024

Other Metrics

View Author Metrics

Citations

Cited By

Kechagia MDevroey XPanichella AGousios Gvan Deursen AZhang DMøller A(2019)Effective and efficient API misuse detection via exception propagation and search-based testingProceedings of the 28th ACM SIGSOFT International Symposium on Software Testing and Analysis10.1145/3293882.3330552(192-203)Online publication date: 10-Jul-2019
https://dl.acm.org/doi/10.1145/3293882.3330552
Allen NKrishnan PScholz BMøller ANaik M(2015)Combining type-analysis with points-to analysis for analyzing Java library source-codeProceedings of the 4th ACM SIGPLAN International Workshop on State Of the Art in Program Analysis10.1145/2771284.2771287(13-18)Online publication date: 14-Jun-2015
https://dl.acm.org/doi/10.1145/2771284.2771287
Wang RZhou YChen SQadeer SEvans DGurevich YKing S(2013)Explicating SDKsProceedings of the 22nd USENIX conference on Security10.5555/2534766.2534801(399-414)Online publication date: 14-Aug-2013
https://dl.acm.org/doi/10.5555/2534766.2534801
Spishak EDietl WErnst MChin WHobor A(2012)A type system for regular expressionsProceedings of the 14th Workshop on Formal Techniques for Java-like Programs10.1145/2318202.2318207(20-26)Online publication date: 12-Jun-2012
https://dl.acm.org/doi/10.1145/2318202.2318207

View Options

View options

Get Access

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

Media

Figures

Other

Tables

View Issue’s Table of Contents