sinancepel

The reasons turn out to be decently boring here. Zoncolan [0] and Pyre [1], which Pysa shares core libraries with, are also written in OCaml, and the language made sense to use from the perspective of both sharing code and having people who are proficient and comfortable writing in OCaml working on the project.

[0]: https://engineering.fb.com/security/zoncolan/

[1]: https://github.com/facebook/pyre-check

The article briefly mentions this, although it might not be super clear from the short description - "We regularly review issues reported through other avenues, such as our bug bounty program, to ensure that we correct any false negatives." We rely on these mechanisms to find places where we're missing taint coverage and write sources and sinks as necessary. As of right now, all the annotations are manual.

I hadn't looked too deeply into the literature there, the paper looks really interesting! We don't have any concrete plans to implement such a system, but I don't think there's any fundamental reason we wouldn't want automatic taint model generation. I'll give the paper a read on Monday to learn more :)

Pyre & Pysa try to do a best-effort analysis of Python 2, and supports Python 2 style taint annotations, but most of the code we analyze at Facebook is Python 3.6+.

For Instagram (millions of LOC), the analysis gives feedback to engineers in about 65 minutes on average - note that this is in the context of a diff run: We compare the results of a run on the base revision to the proposed changes, running the tool once or twice depending on whether we hit the cache. It's hard to say how long it'll take on your repository as it depends on a lot of factors, but hopefully that provides some intuition.

Pysa will try to analyze all functions regardless of whether they have type hints, but it work better if the function under consideration is typed. Namely, without type hints, it won't be able to pick up on tainted method calls or attribute accesses. However, regular function calls, etc. and standard data structures like dicts and lists should still be tracked normally.

1. Pysa should work without watchman - it shares some code and infrastructure with Pyre, but doesn't need Watchman to complete its analysis.

2. Hopefully the answer to (1) helps here. Pysa shares some code with Pyre, including the parallelization infrastructure - the same infrastructure that makes Pyre fast interactively makes Pysa fast on large codebases. Living on the Pyre GitHub repo allows Pysa to use the parallelization infra, in addition to the type checking APIs of Pyre as necessary.

See also our original post introducing Pyre - our goal from the outset was to build a platform for deeper static analyses: https://www.facebook.com/notes/protect-the-graph/pyre-fast-t...

One of the authors of the blog post and software engineer working on Pysa here - happy to answer any questions you may have :)

If you're interested in the details of how pyre handles generics, unions, etc., you can take a look at the end-to-end typechecking tests, which provide lots of examples: https://github.com/facebook/pyre-check/blob/master/analysis/...

You can have multi-threaded OCaml (our server actually has two threads), but only one can run at a time currently. We solve this problem by having a multi-process architecture where workers only communicate through a lock-free hash table in shared memory.

If you're having trouble with pip, I'd recommend trying `pip3.6 install pyre-check`.

Yes! Pyre adopts types from the typing module, and relies on typeshed[1] to infer types for standard library functions.

[1]: https://github.com/python/typeshed

Exactly - the LSP portion of pyre works for files you have open in an editor, but might miss changes due to a rebase or files you edit on the terminal. The watchman integration is there to make sure that pyre's aware of changes outside your editor.

Edit: pyre will show type errors for all files in your repository, not just the ones you have open.