The Lisa Plugin uses the "Library for Static Analysis", LiSA, developed and maintained by the Software and System Verification (SSV) group at Universita Ca' Foscari in Venice, Italy, (lisa-analyzer.github.io), to implement and run static analyzers based on the theory of Abstract Interpretation.
If MavenCentral is accessible, the gradle build command will download the requisite LiSA libraries. Otherwise, you should install them and add them to the relevant build paths. Add the Lisa and Taint plugins to your project in the usual way. (The various analyses are started using the "default taint query" button in Decompiler.)
The analysis to run is chosen via the Edit → ToolOptions, which gives you a default category Abstract Interpretation and two subcategories Abstract Interpretation/Domains and Abstract Interpretation/Output. Domains is the most important of these, as it provides the list of available analyses.
Domains has three options, corresponding to the choice of Heap, Type, and Value domains, the last being the option you are most likely to want to change.
The symbolic state of an analysis is the combination of these domains.
Output has several options (not well-tested), which correspond to fields in the LiSAConfiguration class.
Abstract Interpretation (the base option set) has additional execution-related options, associated again with LiSAConfiguration.
For the most part, these options may be left to their defaults. However, specific analyses may benefit from different choices.
By default, an analysis uses the current function and its callees as the basis for the analysis. Under certain circumstances, you may want to add additional functions to the base. This action generates control-flow graphs for the current function and its descendants without invoking a particular analysis.
Successive analyses will add to the set of control-flow graphs under consideration without clearing the previous results. To clear previous CFGs, you must explicitly do so. This action removes all active CFGs.
For the "Taint" and "ThreeLevelTaint" analyses, you will need to specify sources of taint. There are two ways to do this. From the decompiler, you may use the normal taint analysis functions (or this action) to specify SOURCES of taint. (SINKS and GATES may also be used, but be aware they currently correspond only to "clean" annotations in LiSA.) Alternatively, from the disassembly view, you may use this action on a line of PCode to mark an input to the op, or on a line of disassembly to get a dialog for entering the varnode ID by hand. The varnode should be specified using its address, e.g. "register:00000000" for RAX.
Using either method may be imprecise. In particular, the analysis currently uses the low PCode, so tokens selected in the decompiler (high PCode) may or may not have an equivalent. Similarly, varnodes marked in the disassembly are inputs only. Marking an input as a source does not mark it as tainted in the analysis' state. In most cases, the resulting output will be tainted, but not future references to the input, e.g. "(unique:5) INT_ADD (register:4), 0x12" taints future references to (unique:5) but not to (register:4).
Note: with the exception of reaching, liveness, and non-interference domains, these domains have been extended (to a greater or lesser extent) to handle p-code. Modifications may not be in sync with the latest domain definitions in the original LiSA analysis archive.
Results are passed, by default, via SARIF to a results table. The functionality of the table is described in more detail in Decompiler Taint Operations. In general, you'll want to enable the "name", "type", "value", and "displayName" columns, as well as "Address" and possibly "location".