4 Search Results for "Milanova, Ana"

Document
DOI: 10.4230/LIPIcs.ECOOP.2025.18
Practical Type-Based Taint Checking and Inference

Authors: Nima Karimipour, Kanak Das, Manu Sridharan, and Behnaz Hassanshahi

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

Abstract
Many important security properties can be formulated in terms of flows of tainted data, and improved taint analysis tools to prevent such flows are of critical need. Most existing taint analyses use whole-program static analysis, leading to scalability challenges. Type-based checking is a promising alternative, as it enables modular and incremental checking for fast performance. However, type-based approaches have not been widely adopted in practice, due to challenges with false positives and annotating existing codebases. In this paper, we present a new approach to type-based checking of taint properties that addresses these challenges, based on two key techniques. First, we present a new type-based tainting checker with significantly reduced false positives, via more practical handling of third-party libraries and other language constructs. Second, we present a novel technique to automatically infer tainting type qualifiers for existing code. Our technique supports inference of generic type argument annotations, crucial for tainting properties. We implemented our techniques in a tool TaintTyper and evaluated it on real-world benchmarks. TaintTyper exceeds the recall of a state-of-the-art whole-program taint analyzer, with comparable precision, and 2.93X-22.9X faster checking time. Further, TaintTyper infers annotations comparable to those written by hand, suitable for insertion into source code. TaintTyper is a promising new approach to efficient and practical taint checking.
Cite as

Nima Karimipour, Kanak Das, Manu Sridharan, and Behnaz Hassanshahi. Practical Type-Based Taint Checking and Inference. In 39th European Conference on Object-Oriented Programming (ECOOP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 333, pp. 18:1-18:25, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{karimipour_et_al:LIPIcs.ECOOP.2025.18,
  author =	{Karimipour, Nima and Das, Kanak and Sridharan, Manu and Hassanshahi, Behnaz},
  title =	{{Practical Type-Based Taint Checking and Inference}},
  booktitle =	{39th European Conference on Object-Oriented Programming (ECOOP 2025)},
  pages =	{18:1--18:25},
  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.18},
  URN =		{urn:nbn:de:0030-drops-233119},
  doi =		{10.4230/LIPIcs.ECOOP.2025.18},
  annote =	{Keywords: Static analysis, Taint Analysis, Pluggable type systems, Security, Inference}
}
Document
DOI: 10.4230/LIPIcs.ECOOP.2025.27
PoTo: A Hybrid Andersen’s Points-To Analysis for Python

Authors: Ingkarat Rak-amnouykit, Ana Milanova, Guillaume Baudart, Martin Hirzel, and Julian Dolby

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

Abstract
As Python is increasingly being adopted for large and complex programs, the importance of static analysis for Python (such as type inference) grows. Unfortunately, static analysis for Python remains a challenging task due to its dynamic language features and its abundant external libraries. To help fill this gap, this paper presents PoTo, an Andersen-style context-insensitive and flow-insensitive points-to analysis for Python. PoTo addresses Python-specific challenges and works for large programs via a novel hybrid evaluation, integrating traditional static points-to analysis with concrete evaluation in the Python interpreter for external library calls. We evaluate the analysis with two clients: type inference and call graph construction. This paper presents PoTo+, a static type inference for Python built on PoTo. We evaluate PoTo+ and compare it to two state-of-the-art Python type inference techniques: (1) the static rule-based Pytype and (2) the deep-learning based DLInfer. Our results show that PoTo+ outperforms both Pytype and DLInfer on existing Python packages. This paper also presents PoToCG, a call-graph construction analysis for Python built on PoTo. We compare PoToCG to PyCG, the state of the art for this problem, and show that PoTo produces more complete and more precise call graphs.
Cite as

Ingkarat Rak-amnouykit, Ana Milanova, Guillaume Baudart, Martin Hirzel, and Julian Dolby. PoTo: A Hybrid Andersen’s Points-To Analysis for Python. In 39th European Conference on Object-Oriented Programming (ECOOP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 333, pp. 27:1-27:29, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{rakamnouykit_et_al:LIPIcs.ECOOP.2025.27,
  author =	{Rak-amnouykit, Ingkarat and Milanova, Ana and Baudart, Guillaume and Hirzel, Martin and Dolby, Julian},
  title =	{{PoTo: A Hybrid Andersen’s Points-To Analysis for Python}},
  booktitle =	{39th European Conference on Object-Oriented Programming (ECOOP 2025)},
  pages =	{27:1--27:29},
  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.27},
  URN =		{urn:nbn:de:0030-drops-233194},
  doi =		{10.4230/LIPIcs.ECOOP.2025.27},
  annote =	{Keywords: Python, Points-to analysis, Machine learning libraries}
}
Document
DOI: 10.4230/LIPIcs.ECOOP.2018.25
Definite Reference Mutability

Authors: Ana Milanova

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

Abstract
Reference immutability type systems such as Javari and ReIm ensure that a given reference cannot be used to mutate the referenced object. These systems are conservative in the sense that a mutable reference may be mutable due to approximation. In this paper, we present ReM (for definite Re[ference] M[utability]). It separates mutable references into (1) definitely mutable, and (2) maybe mutable, i.e., references whose mutability is due to inherent approximation. In addition, we propose a CFL-reachability system for reference immutability, and prove that it is equivalent to ReIm/ReM, thus building a novel framework for reasoning about correctness of reference immutability type systems. We have implemented ReM and applied it on a large benchmark suite. Our results show that approximately 86.5% of all mutable references are definitely mutable.
Cite as

Ana Milanova. Definite Reference Mutability. In 32nd European Conference on Object-Oriented Programming (ECOOP 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 109, pp. 25:1-25:30, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{milanova:LIPIcs.ECOOP.2018.25,
  author =	{Milanova, Ana},
  title =	{{Definite Reference Mutability}},
  booktitle =	{32nd European Conference on Object-Oriented Programming (ECOOP 2018)},
  pages =	{25:1--25:30},
  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.25},
  URN =		{urn:nbn:de:0030-drops-92303},
  doi =		{10.4230/LIPIcs.ECOOP.2018.25},
  annote =	{Keywords: reference immutability, type inference, CFL-reachability, precision}
}
Document
DOI: 10.4230/DARTS.4.3.7
Definite Reference Mutability (Artifact)

Authors: Ana Milanova and Wei Huang

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

Abstract
Related paper "Definite Reference Mutability" presents ReM (Re[ference] M[utability]), a type system that separates mutable references into (1) definitely mutable, and (2) maybe mutable, i.e., references whose mutability is due to inherent approximation. We have implemented ReM and applied it on a large benchmark suite. Results show that ~ 86\% of mutable references are definitely mutable. This article describes the tool artifact from the related paper. The purpose of the article and artifact is to allow researchers to reproduce our results, as well as build new type systems upon our code.
Cite as

Ana Milanova and Wei Huang. Definite Reference Mutability (Artifact). In Special Issue of the 32nd European Conference on Object-Oriented Programming (ECOOP 2018). Dagstuhl Artifacts Series (DARTS), Volume 4, Issue 3, pp. 7:1-7:3, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@Article{milanova_et_al:DARTS.4.3.7,
  author =	{Milanova, Ana and Huang, Wei},
  title =	{{Definite Reference Mutability (Artifact)}},
  pages =	{7:1--7:3},
  journal =	{Dagstuhl Artifacts Series},
  ISSN =	{2509-8195},
  year =	{2018},
  volume =	{4},
  number =	{3},
  editor =	{Milanova, Ana and Huang, Wei},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DARTS.4.3.7},
  URN =		{urn:nbn:de:0030-drops-92382},
  doi =		{10.4230/DARTS.4.3.7},
  annote =	{Keywords: reference immutability, type inference, CFL-reachability}
}
  • Refine by Type
  • 4 Document/PDF
  • 1 Document/HTML

  • Refine by Publication Year
  • 2 2025
  • 2 2018

  • Refine by Author
  • 3 Milanova, Ana
  • 1 Baudart, Guillaume
  • 1 Das, Kanak
  • 1 Dolby, Julian
  • 1 Hassanshahi, Behnaz
  • Show More...

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

  • Refine by Classification
  • 2 Software and its engineering → General programming languages
  • 1 Security and privacy → Software security engineering
  • 1 Software and its engineering → Software verification and validation
  • 1 Theory of computation → Program analysis

  • Refine by Keyword
  • 2 CFL-reachability
  • 2 reference immutability
  • 2 type inference
  • 1 Inference
  • 1 Machine learning libraries
  • 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