K-Taint: A Static Taint Analyzer in the K Framework

K-Taint is a rewriting logic-based executable semantics in the K framework for taint analysis of an imperative programming language.

How to run

• Download "Lang.k" under "./src"
• Open: http://www.kframework.org/tool/run/
• On the right panel of the workspace, create a directory and upload "Lang.k" and an input program (sample programs can be found in "./Experiments/TestCodes/")
• Click on "Compile" and then on "Run"

Contributors

• Developed By: Md. Imran Alam and Harshita Goswami
• Release Date: December 2017
• Contact: imran.pcs16@iitp.ac.in / mdimranalam061@gmail.com

References

1. Md. Imran Alam, Raju Halder, Harshita Goswami, and Jorge Sousa Pinto. K-Taint: An Executable Rewriting Logic Semantics for Taint Analysis in the K Framework. Proc. of the 13th International Conference on Evaluation of Novel Approaches to Software Engineering (ENASE '18), Pages 359-366. Funchal, Madeira, Portugal, 23-25 Mar 2018. SciTePress.

2. Rosu, G., Serbanuta, T.F.: An overview of the K semantic framework. The Journal of Logic and Algebraic Programming 79(6), 397–434 (2010)

3. The K framework: http://www.kframework.org/index.php/Main_Page

4. Hunt, S., Sands, D.: On flow-sensitive security types. In: Conf. Record of the 33rd ACM SIGPLAN-SIGACT Sym. on POPL. pp. 79–90. ACM, S. California (2006)