5 Search Results for "Späth, Johannes"

Document
DOI: 10.4230/LIPIcs.ECOOP.2025.34
Taming and Dissecting Recursions Through Interprocedural Weak Topological Ordering

Authors: Jiawei Yang, Xiao Cheng, Bor-Yuh Evan Chang, Xiapu Luo, and Yulei Sui

Published in: LIPIcs, Volume 333, 39th European Conference on Object-Oriented Programming (ECOOP 2025)

Abstract
Abstract interpretation provides a foundational framework for approximating program semantics by interpreting code through abstract domains using semantic functions over ordered sets along a program’s control flow graph (CFG). To facilitate fixpoint computation in abstract interpretation, weak topological ordering (WTO) is an effective strategy for handling loops, as it identifies strategic control points in the CFG where widening and narrowing operations should be applied. However, existing abstract interpreters still face challenges when extending WTO computation in the presence of recursive programs. Computing a precise whole-program WTO requires full context-sensitive analysis which is not scalable for large programs, while context-insensitive analysis introduces spurious cycles that compromise precision. Current approaches either ignore recursion (resulting in unsoundness) or rely on conservative approximations, sacrificing precision by adopting the greatest elements of abstract domains and applying widening at function boundaries without subsequent narrowing refinements. These can lead to undesired results for downstream tasks, such as bug detection. To address the above limitations, we present RecTopo, a new technique to boost the efficiency of precise abstract interpretation in the presence of recursive programs through interprocedural weak topological ordering (IWTO). Rather than pursuing an expensive whole-program WTO analysis, RecTopo employs an on-demand approach that strategically decomposes programs at recursion boundaries and constructs targeted IWTOs for each recursive component. RecTopo dissects and analyzes (nested) recursions through interleaved widening and narrowing operations. This approach enables precise control over interpretation ordering within recursive structures while eliminating spurious recursions through systematic correlation of control flow and call graphs. We implemented RecTopo and evaluated its effectiveness using an assertion-based checking client focused on buffer overflow detection, comparing it against three popular open-source abstract interpreters (IKOS, Clam, CSA). The experiments on 8312 programs from the NIST dataset demonstrate that, on average, RecTopo is 31.99% more precise and achieves a 17.49% higher recall rate compared to three other tools. Moreover, RecTopo exhibits an average precision improvement of 46.51% and a higher recall rate of 32.98% compared to our baselines across ten large open-source projects. Further ablation studies reveal that IWTO reduces spurious widening operations compared to whole-program WTO, resulting in a 12.83% reduction in analysis time.
Cite as

Jiawei Yang, Xiao Cheng, Bor-Yuh Evan Chang, Xiapu Luo, and Yulei Sui. Taming and Dissecting Recursions Through Interprocedural Weak Topological Ordering. In 39th European Conference on Object-Oriented Programming (ECOOP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 333, pp. 34:1-34:31, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{yang_et_al:LIPIcs.ECOOP.2025.34,
  author =	{Yang, Jiawei and Cheng, Xiao and Chang, Bor-Yuh Evan and Luo, Xiapu and Sui, Yulei},
  title =	{{Taming and Dissecting Recursions Through Interprocedural Weak Topological Ordering}},
  booktitle =	{39th European Conference on Object-Oriented Programming (ECOOP 2025)},
  pages =	{34:1--34:31},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-373-7},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{333},
  editor =	{Aldrich, Jonathan and Silva, Alexandra},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2025.34},
  URN =		{urn:nbn:de:0030-drops-233265},
  doi =		{10.4230/LIPIcs.ECOOP.2025.34},
  annote =	{Keywords: Abstract interpretation, recursion, weak topological ordering}
}
Document
DOI: 10.4230/LIPIcs.ECOOP.2018.10
CrySL: An Extensible Approach to Validating the Correct Usage of Cryptographic APIs

Authors: Stefan Krüger, Johannes Späth, Karim Ali, Eric Bodden, and Mira Mezini

Published in: LIPIcs, Volume 109, 32nd European Conference on Object-Oriented Programming (ECOOP 2018)

Abstract
Various studies have empirically shown that the majority of Java and Android apps misuse cryptographic libraries, causing devastating breaches of data security. It is crucial to detect such misuses early in the development process. To detect cryptography misuses, one must first define secure uses, a process mastered primarily by cryptography experts, and not by developers. In this paper, we present CrySL, a definition language for bridging the cognitive gap between cryptography experts and developers. CrySL enables cryptography experts to specify the secure usage of the cryptographic libraries that they provide. We have implemented a compiler that translates such CrySL specification into a context-sensitive and flow-sensitive demand-driven static analysis. The analysis then helps developers by automatically checking a given Java or Android app for compliance with the CrySL-encoded rules. We have designed an extensive CrySL rule set for the Java Cryptography Architecture (JCA), and empirically evaluated it by analyzing 10,000 current Android apps. Our results show that misuse of cryptographic APIs is still widespread, with 95% of apps containing at least one misuse. Our easily extensible CrySL rule set covers more violations than previous special-purpose tools with hard-coded rules, with our tooling offering a more precise analysis.
Cite as

Stefan Krüger, Johannes Späth, Karim Ali, Eric Bodden, and Mira Mezini. CrySL: An Extensible Approach to Validating the Correct Usage of Cryptographic APIs. In 32nd European Conference on Object-Oriented Programming (ECOOP 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 109, pp. 10:1-10:27, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{kruger_et_al:LIPIcs.ECOOP.2018.10,
  author =	{Kr\"{u}ger, Stefan and Sp\"{a}th, Johannes and Ali, Karim and Bodden, Eric and Mezini, Mira},
  title =	{{CrySL: An Extensible Approach to Validating the Correct Usage of Cryptographic APIs}},
  booktitle =	{32nd European Conference on Object-Oriented Programming (ECOOP 2018)},
  pages =	{10:1--10:27},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-079-8},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{109},
  editor =	{Millstein, Todd},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2018.10},
  URN =		{urn:nbn:de:0030-drops-92151},
  doi =		{10.4230/LIPIcs.ECOOP.2018.10},
  annote =	{Keywords: cryptography, domain-specific language, static analysis}
}
Document
DOI: 10.4230/DARTS.4.3.6
CrySL: An Extensible Approach to Validating the Correct Usage of Cryptographic APIs (Artifact)

Authors: Stefan Krüger, Johannes Späth, Karim Ali, Eric Bodden, and Mira Mezini

Published in: DARTS, Volume 4, Issue 3, Special Issue of the 32nd European Conference on Object-Oriented Programming (ECOOP 2018)

Abstract
In this artefact, we present CrySL, an extensible approach to validating the correct usage of cryptographic APIs. The artefact contains executables for CogniCrypt_{SAST}, the analysis CrySL-based analysis, along with the CrySL rules we used in in the original paper's experiments. We also provide scripts to re-run the experiments. We finally include a tutorial to showcase the CogniCrypt_{SAST} on a small Java target program.
Cite as

Stefan Krüger, Johannes Späth, Karim Ali, Eric Bodden, and Mira Mezini. CrySL: An Extensible Approach to Validating the Correct Usage of Cryptographic APIs (Artifact). In Special Issue of the 32nd European Conference on Object-Oriented Programming (ECOOP 2018). Dagstuhl Artifacts Series (DARTS), Volume 4, Issue 3, pp. 6:1-6:4, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@Article{kruger_et_al:DARTS.4.3.6,
  author =	{Kr\"{u}ger, Stefan and Sp\"{a}th, Johannes and Ali, Karim and Bodden, Eric and Mezini, Mira},
  title =	{{CrySL: An Extensible Approach to Validating the Correct Usage of Cryptographic APIs (Artifact)}},
  pages =	{6:1--6:4},
  journal =	{Dagstuhl Artifacts Series},
  ISSN =	{2509-8195},
  year =	{2018},
  volume =	{4},
  number =	{3},
  editor =	{Kr\"{u}ger, Stefan and Sp\"{a}th, Johannes and Ali, Karim and Bodden, Eric and Mezini, Mira},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DARTS.4.3.6},
  URN =		{urn:nbn:de:0030-drops-92371},
  doi =		{10.4230/DARTS.4.3.6},
  annote =	{Keywords: cryptography, domain-specific language, static analysis}
}
Document
DOI: 10.4230/LIPIcs.ECOOP.2016.22
Boomerang: Demand-Driven Flow- and Context-Sensitive Pointer Analysis for Java

Authors: Johannes Späth, Lisa Nguyen Quang Do, Karim Ali, and Eric Bodden

Published in: LIPIcs, Volume 56, 30th European Conference on Object-Oriented Programming (ECOOP 2016)

Abstract
Many current program analyses require highly precise pointer information about small, tar- geted parts of a given program. This motivates the need for demand-driven pointer analyses that compute information only where required. Pointer analyses generally compute points-to sets of program variables or answer boolean alias queries. However, many client analyses require richer pointer information. For example, taint and typestate analyses often need to know the set of all aliases of a given variable under a certain calling context. With most current pointer analyses, clients must compute such information through repeated points-to or alias queries, increasing complexity and computation time for them. This paper presents Boomerang, a demand-driven, flow-, field-, and context-sensitive pointer analysis for Java programs. Boomerang computes rich results that include both the possible allocation sites of a given pointer (points-to information) and all pointers that can point to those allocation sites (alias information). For increased precision and scalability, clients can query Boomerang with respect to particular calling contexts of interest. Our experiments show that Boomerang is more precise than existing demand-driven pointer analyses. Additionally, using Boomerang, the taint analysis FlowDroid issues up to 29.4x fewer pointer queries compared to using other pointer analyses that return simpler pointer infor- mation. Furthermore, the search space of Boomerang can be significantly reduced by requesting calling contexts from the client analysis.
Cite as

Johannes Späth, Lisa Nguyen Quang Do, Karim Ali, and Eric Bodden. Boomerang: Demand-Driven Flow- and Context-Sensitive Pointer Analysis for Java. In 30th European Conference on Object-Oriented Programming (ECOOP 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 56, pp. 22:1-22:26, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{spath_et_al:LIPIcs.ECOOP.2016.22,
  author =	{Sp\"{a}th, Johannes and Nguyen Quang Do, Lisa and Ali, Karim and Bodden, Eric},
  title =	{{Boomerang: Demand-Driven Flow- and Context-Sensitive Pointer Analysis for Java}},
  booktitle =	{30th European Conference on Object-Oriented Programming (ECOOP 2016)},
  pages =	{22:1--22:26},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-014-9},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{56},
  editor =	{Krishnamurthi, Shriram and Lerner, Benjamin S.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2016.22},
  URN =		{urn:nbn:de:0030-drops-61164},
  doi =		{10.4230/LIPIcs.ECOOP.2016.22},
  annote =	{Keywords: Demand-Driven; Static Analysis; IFDS; Aliasing; Points-to Analysis}
}
Document
DOI: 10.4230/DARTS.2.1.12
Boomerang: Demand-Driven Flow- and Context-Sensitive Pointer Analysis for Java (Artifact)

Authors: Johannes Späth, Lisa Nguyen Quang Do, Karim Ali, and Eric Bodden

Published in: DARTS, Volume 2, Issue 1, Special Issue of the 30th European Conference on Object-Oriented Programming (ECOOP 2016)

Abstract
Evaluating pointer analyses with respect to soundness and precision has been a tedious task. Within this artifact we present PointerBench, the benchmark suite used in the paper to compare the pointer analysis Boomerang with two other demand-driven pointer analyses, SB [Sridharan and Bodik, 2006] and DA [Yan et al., 2011]. We show PointerBench can be used to test different pointer analyses. In addition to that, the artifact contains usage examples for Boomerang on simple test programs. The test programs and the input on these programs to Boomerang can be changed to experiment with the algorithm and its features. Additionally, the artifact contains the integration of Boomerang, SB, and DA into FlowDroid, which can then be executed on arbitrary Android applications.
Cite as

Johannes Späth, Lisa Nguyen Quang Do, Karim Ali, and Eric Bodden. Boomerang: Demand-Driven Flow- and Context-Sensitive Pointer Analysis for Java (Artifact). In Special Issue of the 30th European Conference on Object-Oriented Programming (ECOOP 2016). Dagstuhl Artifacts Series (DARTS), Volume 2, Issue 1, pp. 12:1-12:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@Article{spath_et_al:DARTS.2.1.12,
  author =	{Sp\"{a}th, Johannes and Nguyen Quang Do, Lisa and Ali, Karim and Bodden, Eric},
  title =	{{Boomerang: Demand-Driven Flow- and Context-Sensitive Pointer Analysis for Java (Artifact)}},
  pages =	{12:1--12:2},
  journal =	{Dagstuhl Artifacts Series},
  ISSN =	{2509-8195},
  year =	{2016},
  volume =	{2},
  number =	{1},
  editor =	{Sp\"{a}th, Johannes and Nguyen Quang Do, Lisa and Ali, Karim and Bodden, Eric},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DARTS.2.1.12},
  URN =		{urn:nbn:de:0030-drops-61334},
  doi =		{10.4230/DARTS.2.1.12},
  annote =	{Keywords: Demand-Driven; Static Analysis; IFDS; Aliasing; Points-to Analysis}
}
  • Refine by Type
  • 5 Document/PDF
  • 1 Document/HTML

  • Refine by Publication Year
  • 1 2025
  • 2 2018
  • 2 2016

  • Refine by Author
  • 4 Ali, Karim
  • 4 Bodden, Eric
  • 4 Späth, Johannes
  • 2 Krüger, Stefan
  • 2 Mezini, Mira
  • Show More...

  • Refine by Series/Journal
  • 3 LIPIcs
  • 2 DARTS

  • Refine by Classification
  • 1 Security and privacy → Software and application security
  • 1 Software and its engineering → Semantics
  • 1 Software and its engineering → Software defect analysis
  • 1 Software and its engineering → Syntax
  • 1 Theory of computation → Program analysis

  • Refine by Keyword
  • 2 Demand-Driven; Static Analysis; IFDS; Aliasing; Points-to Analysis
  • 2 cryptography
  • 2 domain-specific language
  • 2 static analysis
  • 1 Abstract interpretation
  • Show More...

Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2026 Schloss Dagstuhl – LZI GmbH Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact