Added work around for the detection of tainted annotations during the analysis of PRIVATE_STATES_IN_OTHER_PRIVATE_STATES

Author: olivieriluca

go-lisa/src/main/java/it/unive/golisa/GoLiSA.java

@@ -200,7 +200,6 @@ public static void main(String[] args) throws AnalysisSetupException, IOExceptio
 			res[3] = satisfyPhaseRequirements(program, PRIVATE_STATES_IN_PUBLIC_STATES);
 			res[4] = satisfyPhaseRequirements(program, PRIVATE_STATES_IN_OTHER_PRIVATE_STATES);
 
-		
 			if(res[0])
 				runInformationFlowAnalysis(program, entryLoader, outputDir, dumpOpt, PRIVATE_INPUT_IN_PUBLIC_STATES, PrivacySignatures.privateInputs, PrivacySignatures.publicWriteStatesAndResponsesWithCriticalParams);
 			else 
@@ -221,7 +220,7 @@ public static void main(String[] args) throws AnalysisSetupException, IOExceptio
 				runInformationFlowAnalysis(program, entryLoader, outputDir, dumpOpt, PRIVATE_STATES_IN_PUBLIC_STATES, PrivacySignatures.privateReadStates, PrivacySignatures.publicWriteStatesAndResponsesWithCriticalParams);
 			else 
 				LOG.info("Program does not contains at least a source and sink for phase " + PRIVATE_STATES_IN_PUBLIC_STATES);
-			
+
 			if(res[4])
 				runAnalysesForPrivateInOtherPrivateStates(program, entryLoader, outputDir, dumpOpt, policyPath);	
 
@@ -499,13 +498,16 @@ private static void runInformationFlowAnalysis(Program program, EntryPointLoader
 
 		Set<Triple<CallType, ? extends CodeAnnotation, CodeMemberDescriptor>> specificCodeMemberAnnotations = new HashSet<>() ;
 
+		TaintDomainForPrivacyHF.TAINTED_ANNOTATION.cleanSources();
+		
 		Set<Call> sourcesTocheckRawData = new HashSet<>();
 		for(Call source : sources) {
 			Set<CodeMemberDescriptor> descriptors = getCodeMemberDescriptors(source);
 			if(descriptors.isEmpty())
 				sourcesTocheckRawData.add(source);
 			else
 				for(CodeMemberDescriptor d : descriptors) {
+					TaintDomainForPrivacyHF.TAINTED_ANNOTATION.addSource(source);
 					specificCodeMemberAnnotations.add(Triple.of(source.getCallType(), new MethodAnnotation(TaintDomainForPrivacyHF.TAINTED_ANNOTATION, d.getUnit().getName(), d.getName()), d));
 				}
 		}

go-lisa/src/main/java/it/unive/golisa/analysis/taint/SourceTrackTaintAnnotation.java

@@ -0,0 +1,35 @@
+package it.unive.golisa.analysis.taint;
+
+import java.util.HashSet;
+import java.util.Set;
+
+import it.unive.lisa.program.annotations.Annotation;
+
+import it.unive.lisa.program.cfg.statement.Statement;
+
+public class SourceTrackTaintAnnotation extends Annotation {
+	
+	private final Set<Statement> sources;
+	
+	public SourceTrackTaintAnnotation(String annotationName) {
+		super(annotationName);
+		sources = new HashSet<>();
+	}
+
+	public Set<Statement> getSources() {
+		return new HashSet<>(sources);
+	}
+
+	public void addSources(Set<Statement> sources) {
+		this.sources.addAll(sources);
+	}
+	
+	public void addSource(Statement source) {
+		this.sources.add(source);
+	}
+	
+	public void cleanSources() {
+		sources.clear();
+	}
+
+}

go-lisa/src/main/java/it/unive/golisa/analysis/taint/TaintDomainForPrivacyHF.java

@@ -16,6 +16,7 @@
 import it.unive.lisa.program.annotations.matcher.AnnotationMatcher;
 import it.unive.lisa.program.annotations.matcher.BasicAnnotationMatcher;
 import it.unive.lisa.program.cfg.ProgramPoint;
+import it.unive.lisa.program.cfg.statement.Statement;
 import it.unive.lisa.symbolic.SymbolicExpression;
 import it.unive.lisa.symbolic.value.Constant;
 import it.unive.lisa.symbolic.value.Identifier;
@@ -42,7 +43,7 @@ public TaintDomainForPrivacyHF evalPushAny(PushAny pushAny, ProgramPoint pp, Sem
 	/**
 	 * The annotation Tainted.
 	 */
-	public static final Annotation TAINTED_ANNOTATION = new Annotation("lisa.taint.Tainted");
+	public static final SourceTrackTaintAnnotation TAINTED_ANNOTATION = new SourceTrackTaintAnnotation("lisa.taint.Tainted");
 
 	/**
 	 * The matcher for the Tainted annotation.
@@ -105,8 +106,17 @@ public TaintDomainForPrivacyHF fixedVariable(Identifier id, ProgramPoint pp, Sem
 		if (annots.isEmpty())
 			return BaseNonRelationalValueDomain.super.fixedVariable(id, pp, oracle);
 
-		if (annots.contains(TAINTED_MATCHER))
-			return TAINTED;
+		for(Annotation a : annots)
+			if (TAINTED_MATCHER.matches(a)) {
+				if(a instanceof SourceTrackTaintAnnotation) {
+	 				SourceTrackTaintAnnotation stta = (SourceTrackTaintAnnotation) a;
+	 				for(Statement src : stta.getSources())
+	 					if(src.getLocation().equals(pp.getLocation()))
+	 						return TAINTED;
+				} else 
+					return TAINTED;
+			}
+		
 
 		if (annots.contains(CLEAN_MATCHER))
 			return CLEAN;

go-lisa/src/main/java/it/unive/golisa/checker/ComputePrivateCollectionFromStatementsChecker.java

@@ -1,11 +1,13 @@
 package it.unive.golisa.checker;
 
+import java.util.Collection;
 import java.util.HashMap;
 import java.util.HashSet;
 import java.util.List;
 import java.util.Map;
 import java.util.Set;
 
+import it.unive.golisa.analysis.taint.TaintDomainForPrivacyHF;
 import it.unive.golisa.analysis.utilities.PrivacySignatures;
 import it.unive.golisa.cfg.utils.CFGUtils;
 import it.unive.lisa.analysis.AnalysisState;
@@ -25,6 +27,7 @@
 import it.unive.lisa.program.cfg.edge.Edge;
 import it.unive.lisa.program.cfg.statement.Statement;
 import it.unive.lisa.program.cfg.statement.call.Call;
+import it.unive.lisa.program.cfg.statement.call.UnresolvedCall;
 import it.unive.lisa.symbolic.SymbolicExpression;
 import it.unive.lisa.symbolic.value.ValueExpression;
 import it.unive.lisa.type.Type;
@@ -84,9 +87,17 @@ public boolean visit(CheckToolWithAnalysisResults<SimpleAbstractState<PointBased
 					}
 
 					if(PrivacySignatures.isReadPrivateState(call)) {
-						readers.put(call,collectionValue);
+						Collection<AnalyzedCFG<SimpleAbstractState<PointBasedHeap, ValueEnvironment<Tarsis>, TypeEnvironment<InferredTypes>>>> result = tool.getResultOf(call.getCFG());
+						for (AnalyzedCFG<SimpleAbstractState<PointBasedHeap, ValueEnvironment<Tarsis>, TypeEnvironment<InferredTypes>>> analyzedCFG : result) {
+							Call resolved = (Call) tool.getResolvedVersion((UnresolvedCall) call, analyzedCFG);
+							readers.put(resolved,collectionValue);
+						}
 					} else {
-						writers.put(call,collectionValue);
+						Collection<AnalyzedCFG<SimpleAbstractState<PointBasedHeap, ValueEnvironment<Tarsis>, TypeEnvironment<InferredTypes>>>> result = tool.getResultOf(call.getCFG());
+						for (AnalyzedCFG<SimpleAbstractState<PointBasedHeap, ValueEnvironment<Tarsis>, TypeEnvironment<InferredTypes>>> analyzedCFG : result) {
+							Call resolved = (Call) tool.getResolvedVersion((UnresolvedCall) call, analyzedCFG);
+							writers.put(resolved,collectionValue);
+						}
 					}
 
 				} catch (SemanticException e) {