Java
  • About This Book
  • 🍖Prerequisites
    • 反射
      • 反射基本使用
      • 高版本JDK反射绕过
      • 反射调用命令执行
      • 反射构造HashMap
      • 方法句柄
    • 类加载
      • 动态加载字节码
      • 双亲委派模型
      • BCEL
      • SPI
    • RMI & JNDI
      • RPC Intro
      • RMI
      • JEP 290
      • JNDI
    • Misc
      • Unsafe
      • 代理模式
      • JMX
      • JDWP
      • JPDA
      • JVMTI
      • JNA
      • Java Security Manager
  • 👻Serial Journey
    • URLDNS
    • SerialVersionUID
    • Commons Collection 🥏
      • CC1-TransformedMap
      • CC1-LazyMap
      • CC6
      • CC3
      • CC2
    • FastJson 🪁
      • FastJson-Basic Usage
      • FastJson-TemplatesImpl
      • FastJson-JdbcRowSetImpl
      • FastJson-BasicDataSource
      • FastJson-ByPass
      • FastJson与原生反序列化(一)
      • FastJson与原生反序列化(二)
      • Jackson的原生反序列化利用
    • Other Components
      • SnakeYaml
      • C3P0
      • AspectJWeaver
      • Rome
      • Spring
      • Hessian
      • Hessian_Only_JDK
      • Kryo
      • Dubbo
  • 🌵RASP
    • JavaAgent
    • JVM
    • ByteCode
    • JNI
    • ASM 🪡
      • ASM Intro
      • Class Generation
      • Class Transformation
    • Rasp防御命令执行
    • OpenRASP
  • 🐎Memory Shell
    • Tomcat-Architecture
    • Servlet API
      • Listener
      • Filter
      • Servlet
    • Tomcat-Middlewares
      • Tomcat-Valve
      • Tomcat-Executor
      • Tomcat-Upgrade
    • Agent MemShell
    • WebSocket
    • 内存马查杀
    • IDEA本地调试Tomcat
  • ✂️JDBC Attack
    • MySQL JDBC Attack
    • H2 JDBC Attack
  • 🎨Templates
    • FreeMarker
    • Thymeleaf
    • Enjoy
  • 🎏MessageQueue
    • ActiveMQ CNVD-2023-69477
    • AMQP CVE-2023-34050
    • Spring-Kafka CVE-2023-34040
    • RocketMQ CVE-2023-33246
  • 🛡️Shiro
    • Shiro Intro
    • Request URI ByPass
    • Context Path ByPass
    • Remember Me反序列化 CC-Shiro
    • CB1与无CC依赖的反序列化链
  • 🍺Others
    • Deserialization Twice
    • A New Blazer 4 getter RCE
    • Apache Commons Jxpath
    • El Attack
    • Spel Attack
    • C3P0原生反序列化的JNDI打法
    • Log4j
    • Echo Tech
      • SpringBoot Under Tomcat
    • CTF 🚩
      • 长城杯-b4bycoffee (ROME反序列化)
      • MTCTF2022(CB+Shiro绕过)
      • CISCN 2023 西南赛区半决赛 (Hessian原生JDK+Kryo反序列化)
      • CISCN 2023 初赛 (高版本Commons Collections下其他依赖的利用)
      • CISCN 2021 总决赛 ezj4va (AspectJWeaver写字节码文件到classpath)
      • D^3CTF2023 (新的getter+高版本JNDI不出网+Hessian异常toString)
      • WMCTF2023(CC链花式玩法+盲读文件)
      • 第六届安洵杯网络安全挑战赛(CB PriorityQueue替代+Postgresql JDBC Attack+FreeMarker)
  • 🔍Code Inspector
    • CodeQL 🧶
      • Tutorial
        • Intro
        • Module
        • Predicate
        • Query
        • Type
      • CodeQL 4 Java
        • Basics
        • DFA
        • Example
    • SootUp ✨
      • Intro
      • Jimple
      • DFA
      • CG
    • Tabby 🔦
      • install
    • Theory
      • Static Analysis
        • Intro
        • IR & CFG
        • DFA
        • DFA-Foundation
        • Interprocedural Analysis
        • Pointer Analysis
        • Pointer Analysis Foundation
        • PTA-Context Sensitivity
        • Taint Anlysis
        • Datalog
Powered by GitBook
On this page
  • Iterative Algorithm
  • Partial Order
  • poset
  • upper & lower bounds
  • Lattice
  • Semilattice
  • Complete Lattice
  • Product Lattice
  • DFA Framework via Lattice
  • Monotonicity
  • Fixed Point Theorem
  • Relate to Iterative Algorithm
  • May & Must analysis
  • MOP
  • Constant Propagation
  • Worklist algorithm

Was this helpful?

  1. 🔍Code Inspector
  2. Theory
  3. Static Analysis

DFA-Foundation

PreviousDFANextInterprocedural Analysis

Last updated 7 months ago

Was this helpful?

Iterative Algorithm

Here is a classic iterative algorithm template for May & Forward analysis

Let’s view it in another way

  • Given a CFG with k nodes, the iterative algorithm updates OUT[n] for every node n in each iteration.

  • Assume the domain of the values in data flow analysis is V, let’s define a k-tuple: (OUT[n1], OUT[n2], …, OUT[nk]) as an element of set (V1 × V2 … × Vk) denoted as Vk, to hold the values of the analysis after each iteration.

  • Each iteration can be considered as taking an action to map an element of Vk to a new element of Vk, through applying the transfer functions and control-flow handing, abstracted as a function F: Vk → Vk

  • Then the algorithm outputs a series of k-tuples iteratively until a k-tuple is the same as the last one in two consecutive iterations.

X is a fixed point of function F if X = F(X)

We say the iterative algorithm reaches a fixed point.

Partial Order

poset

Some examples of poset:

  • (S, ≤) , S is a set of integers

  • (S, substring) , S is a set of English words

  • (S, subset) , S is the power set of set {a,b,c}

upper & lower bounds

Obviously, as long as there is an upper bound or a lower bound, the corresponding lub and glb also exist.

Lattice

Some examples of lattice:

  • (S, ≤) , S is a set of integers

    • ⊔ means “max”

    • ⊓ means “min”

  • (S, subset) , S is the power set of set {a,b,c}

    • ⊔ means ∪

    • ⊓ means ∩

Semilattice

Complete Lattice

Some examples of complete lattice:

  • (S, ≤) , S is a set of integers

    • × not a complete lattice

    • it has no ⊔S(+∞)

  • (S, subset) , S is the power set of set {a,b,c}

    • √

Note: the definition of bounds implies that the bounds are not necessarily in the subsets (but they must be in the lattice)

A complete lattice is not necessarily a finite lattice!

Product Lattice

DFA Framework via Lattice

The IN and OUT of every node can be seen as a latice.(data flow value)

Data flow analysis can be seen as iteratively applying transfer functions and meet/join operations on the values of a lattice

Monotonicity

Fixed Point Theorem

Proof:

Relate to Iterative Algorithm

two conditions of fixed point theorem:

  • L is finite

  • f is monotonic

If a product lattice Lk is a product of complete(and finite) lattices, i.e., (L, L, …, L), then Lk is also complete (and finite) =》 L is a finite and complete lattice

In each iteration, it is equivalent to think that we apply function F which consists of

  • transfer function fi: L → L for every node

  • join/meet function ⊔/⊓: L×L×L... → L for control-flow influence

How to prove function F is monotonic?

first, transfer function is obviously monotonic(Gen/Kill function is monotonic, IN/OUT never shrinks)

next, prove that ⊔/⊓ is monotonic

When will the algorithm reach the fixed point?

To sum up, we can draw these conclusions:

  1. the iterative algorithm is guaranteed to terminate(reach the fixed point)

  2. There may be more than one solution, but our solution is the best one(least/greatest fixed point)

  3. Worst case of iterations: lattice height × nodes num in CFG

May & Must analysis

What is the meaning of top and bottom?

Take Reaching Definition for example:

Suppose there is a scenario where the program checks the undefine error. We set a dummy definition for each variable, which means that the variable is undefined. Obviously, they should be set to a value of 0 at first, indicating that all undefined variable will not reach this program point. This is an unsafe result because there may be some undefined variables. This is bottom.

For the top, the values are all 1 which means that all definitions may reach. This is a safe but useless result.

We need the fixed point to stay at the safe area and close to the Truth as long as possible. That is, we need the optimal solution.(least/greatest fixed point)

MOP

How precise is our solution?

MOP: Meet Over All Paths

MOP is only a conceptual metric, as it is not practical to enumerate all paths (there may be path explosions).

Bit-vector or Gen/Kill problems(set union/intersection for join/meet) are distributive.

But some analyses are not distributive

Constant Propagation

Given a variable x at program point p, determine whether x is guaranteed to hold a constant value at p.

The OUT of each node in CFG, includes a set of pairs (x, v) where x is a variable and v is the value held by x after that node

Worklist algorithm

an optimization of Iterative Algorithm.

As iteration goes on in the iterative algorithm, we need to apply F to every node even if one node’s OUT changes.

image-20240405093548478
image-20240405094013650
image-20240405094243100
image-20240405094641615
image-20240405094725002
image-20240405094807219
image-20240405094956644
image-20240405095221142
image-20240405095649604
image-20240405095713765
image-20240405100122578
image-20240405101104252
image-20240405101304929
image-20240405103624941
image-20240405103653446
image-20240405103708296
image-20240405103733012
image-20240405104548572
image-20240405104608361
image-20240405111438552
image-20240405111741958
image-20240405120423891
image-20240405120943340
image-20240405121202416
image-20240405125725741
image-20240405143022516
image-20240405143044398
image-20240405143115949
image-20240405143505512
image-20240405143531481
image-20240405143627014
image-20240405144258241