2 ms·

I'm very sure that I'm not the first person to have stumbled across this idea, and I'm sure that lots of much smarter people have written at length about the th

by muglug 6y ago

I'm very sure that I'm not the first person to have stumbled across this idea, and I'm sure that lots of much smarter people have written at length about the theory, but I'm not aware of that theory having been applied to the analysis of interpreted languages, except with Typed Racket. Specifically I don't know of another widely-used static analysis tool for Python, Ruby, PHP, Perl, JS or TypeScript that performs this analysis. I also haven't come across a paper that describes the application of this technique to those languages, which is why I wrote this post – I want others to see its use, and adopt it too.

UncleMeat 6y ago
A few examples of many. Prototyping Symbolic Execution Engines for Interpreted Languages. Bucer, Kinder, Candea - symexec of python ExpoSE: practical symbolic execution of standalone JavaScript. Loring, Mitchell, Kinder - symexec of javascript Path Sensitive Static Analysis of Web Applications for Remote Code Execution Vulnerability Detection, Zheng, Zhang - path sensitive analysis for strings, doing the same sort of value narrowing based on branches for JS. JSAI: A Static Analysis Platform for JavaScript, Kashyap et al. - static analysis of JS support path sensitive analysis. AppReduce, by Google, does condition-based type narrowing for nullability inference on davik bytecode (an untyped interpreted language). I also believe that WALA (which supports JS) supports path-based narrowing. Other than the AppReduce case, these aren't literally the same thing (type narrowing for inferring types in an untyped interpreted language) but they all play in this same space of "collect path conditions to some instruction, convert them into predicates, run some solving on those predicates, and draw a conclusion about the semantics of the program along that path" that you are playing in.
- muglug 6y ago
  Thanks, that's a great collection. The Zheng & Zhang paper is particularly interesting, given it tackles taint analysis and succeeds where Psalm (which also has a taint analysis mode) fails: https://psalm.dev/r/7098c7bb59 https://psalm.dev/r/7098c7bb59. Might try to implement a cut-down version of their method.

by muglug 6y ago

UncleMeat 6y ago

A few examples of many. Prototyping Symbolic Execution Engines for Interpreted Languages. Bucer, Kinder, Candea - symexec of python ExpoSE: practical symbolic execution of standalone JavaScript. Loring, Mitchell, Kinder - symexec of javascript Path Sensitive Static Analysis of Web Applications for Remote Code Execution Vulnerability Detection, Zheng, Zhang - path sensitive analysis for strings, doing the same sort of value narrowing based on branches for JS. JSAI: A Static Analysis Platform for JavaScript, Kashyap et al. - static analysis of JS support path sensitive analysis. AppReduce, by Google, does condition-based type narrowing for nullability inference on davik bytecode (an untyped interpreted language). I also believe that WALA (which supports JS) supports path-based narrowing. Other than the AppReduce case, these aren't literally the same thing (type narrowing for inferring types in an untyped interpreted language) but they all play in this same space of "collect path conditions to some instruction, convert them into predicates, run some solving on those predicates, and draw a conclusion about the semantics of the program along that path" that you are playing in.

muglug 6y ago
Thanks, that's a great collection. The Zheng & Zhang paper is particularly interesting, given it tackles taint analysis and succeeds where Psalm (which also has a taint analysis mode) fails: https://psalm.dev/r/7098c7bb59 https://psalm.dev/r/7098c7bb59. Might try to implement a cut-down version of their method.