[Soot-list] about Heros

Tue Apr 23 03:00:43 EDT 2013

Hi all.

I have never tried what Marc-Andre suggest but it might work. Another option would be to do on-the-fly pointer analysis as was done, for instance, in Andromeda.
http://link.springer.com/chapter/10.1007/978-3-642-37057-1_15#page-1
We recently implemented this to support a taint analysis and it seems to work quite well.

Eric

On 22.04.2013, at 16:17, Marc-André Laverdière-Papineau <marc-andre.laverdiere-papineau at polymtl.ca> wrote:

> Hello,
> 
> You understood my suggestion properly. And you are right, that means to 
> be using the CG information that is context-sensitive to tell Heros what 
> that edge points to.
> 
> If you want to infer that on the fly, I remember the method published by 
> IBM in their Andromeda paper. I think that they are context insensitive.
> http://www.cs.tau.ac.il/~omertrip/fase13/paper.pdf
> 
> I encourage you to have a look at it but, more importantly, to think if 
> this fits the bill, and how you'd improve the method for context 
> sensitivity.
> 
> Also, note that, right now, the Heros solver has flow function factories 
> that are blissfully unaware of the facts that are enabled. I think that 
> the IFDS/IDE framework is designed that way. That means that, if you are 
> interested in conditional edges, you need to either have very special 
> flow functions, or extend the theory and the solver to add introspection.
> 
> Note that Bodden's team did something with BDDs already that give us 
> conditional edges, but I am not sure it would be on-the-fly enough to 
> your liking...
> 
> Marc-André Laverdière-Papineau
> Doctorant - PhD Candidate
> 
> On 13-04-20 02:26 AM, Rohan Padhye wrote:
>> Hi Marc-André,
>> 
>> Are you saying that instead of using "SootMethod" for generic type "M"
>> in Heroes to use "MethodContext" instead? This will create different
>> copies of each method for different contexts and achieve
>> context-sensitive program points.
>> 
>> This sounds like a great idea if you want to incorporate, say, a
>> context-sensitive call graph in IFDS (e.g. use Paddle's call graph
>> instead of Spark's call graph for a more precise analysis).
>> 
>> The problem I see in this is that the number of distinct contexts is
>> actually defined by the call graph - which in turn is based on points-to
>> information. What you would ideally want is to distinguish contexts
>> based on data flow values of your own analysis which you are performing
>> with Heros - what is the gain from distinguishing between contexts of
>> points-to analysis?
>> 
>> 
>> 
>> On 2013-04-20 07:27, Marc-André Laverdière-Papineau wrote:
>>> Hello,
>>> 
>>> I am butting in, because I had on my mind to try context sensitivity
>>> in
>>> IFDS at some point too...
>>> 
>>> The inherent problem with a bounded stack of context strings is that
>>> it
>>> is bounded :)
>>> 
>>> So the problem you mention could be hit even without recursion. I
>>> sort
>>> of remember algorithms to detect recursion, but I'd have to dust off
>>> my
>>> Dragon Book to get in the details of that.
>>> 
>>> The question is: why bother?
>>> 
>>> I am thinking that one may define an IFDS analysis that use the
>>> MethodOrMethodContext API and the Geometric encoding - which removes
>>> the
>>> need for context strings altogether.
>>> 
>>> Marc-André Laverdière-Papineau
>>> Doctorant - PhD Candidate
>>> 
>>> On 13-04-19 09:56 AM, Rohan Padhye wrote:
>>>> Hello Eric,
>>>> 
>>>> That is an interesting approach. I also have a requirement of
>>>> context-sensitive data flow values so allow me to butt into this
>>>> thread.
>>>> 
>>>> How would such a model work in the presence of recursion? Wouldn't
>>>> bounding the call-string stack limit the precision for call
>>>> sequences
>>>> deeper than that bound? And would the algorithmic complexity
>>>> increase by
>>>> a cubic factor of the stack-bound? Or am I getting it wrong?
>>>> 
>>>> Alternatively, if a client wants to query whether a data flow fact
>>>> "x"
>>>> holds at a point "p" along a particular call-sequence "c_1...c_k",
>>>> would
>>>> it make sense (this is just a stab in the dark, I may be absolutely
>>>> wrong) to only compute graph reachability starting from <entry,
>>>> zero> to
>>>> <p, x> along paths that contain the call sequence "c_1...c_k"? Or is
>>>> this an incorrect understanding?
>>>> 
>>>> Thanks,
>>>> Rohan
>>>> 
>>>> On 2013-04-19 15:07, Bodden, Eric wrote:
>>>>> Hi Zhang.
>>>>> 
>>>>> IFDS formulates context-sensitive analysis in such a way that a
>>>>> context is characterized by domain values, not by (method-signature
>>>>> based) calling-context strings. You should hence design your
>>>>> abstract
>>>>> domain accordingly. For instance, in case you really need a
>>>>> calling-context string then your domain should hold a (bounded)
>>>>> stack
>>>>> of those strings.
>>>>> 
>>>>> Eric
>>>>> 
>>>>> 
>>>>> 
>>>>> On 18.04.2013, at 17:46, Zhang Yufeng <yuffonzhang at 163.com> wrote:
>>>>> 
>>>>>> Hi Eric,
>>>>>> I am using Heros in my project.
>>>>>> I have two questions about the "context-sensitive" problem.
>>>>>> 
>>>>>> The first question:
>>>>>> In my IFDS problem,
>>>>>> in implementing the function
>>>>>> public FlowFunction<Local> getNormalFlowFunction(Unit curr, Unit
>>>>>> succ) {}
>>>>>> I need to know the context about where the method including 'curr'
>>>>>> is invoked.
>>>>>> 
>>>>>> In my problem, the operations on the Domain D for the same unit
>>>>>> are
>>>>>> different in different context.
>>>>>> For example, in the following fuction:
>>>>>> 
>>>>>> void foo() {
>>>>>> obj1=obj2;
>>>>>> }
>>>>>> 
>>>>>> for statement
>>>>>> obj1=obj2;
>>>>>> 
>>>>>> the operation on the 'facts' in the domain 'D' is different in the
>>>>>> different context (where the function foo() is invoked).
>>>>>> 
>>>>>> But in the function
>>>>>> public FlowFunction<Local> getNormalFlowFunction(Unit curr, Unit
>>>>>> succ) {}
>>>>>> there is no information indicating that the curr unit is
>>>>>> encountered
>>>>>> under what context.
>>>>>> 
>>>>>> Can I do this in Heros?
>>>>>> 
>>>>>> 
>>>>>> The second question is also about the context-sensitive problem.
>>>>>> After I get the results by solving the IFDS problem.
>>>>>> I can get the result at each unit by using:
>>>>>> solver.resultsAt((Stmt)unit);
>>>>>> right?
>>>>>> My question is:
>>>>>> does Heros keep the context-sensitive information in the results?
>>>>>> In some cases, the results at the same unit are different in
>>>>>> different context.
>>>>>> How can I get this from Heros?
>>>>>> 
>>>>>> I don't know whether I make it clear.
>>>>>> 
>>>>>> Thanks.
>>>>>> Best.
>>>>>> Yufeng
>>>>>> _______________________________________________
>>>>>> Soot-list mailing list
>>>>>> Soot-list at sable.mcgill.ca
>>>>>> http://mailman.cs.mcgill.ca/mailman/listinfo/soot-list
>>>>> 
>>>>> --
>>>>> Eric Bodden, Ph.D., http://sse.ec-spride.de/ http://bodden.de/
>>>>> Head of Secure Software Engineering Group at EC SPRIDE
>>>>> Tel: +49 6151 16-75422    Fax: +49 6151 16-72051
>>>>> Room 3.2.14, Mornewegstr. 30, 64293 Darmstadt
>>>>> 
>>>>> _______________________________________________
>>>>> Soot-list mailing list
>>>>> Soot-list at sable.mcgill.ca
>>>>> http://mailman.cs.mcgill.ca/mailman/listinfo/soot-list
>>>> 
>>>> _______________________________________________
>>>> Soot-list mailing list
>>>> Soot-list at sable.mcgill.ca
>>>> http://mailman.cs.mcgill.ca/mailman/listinfo/soot-list
>>>> 
>>> _______________________________________________
>>> Soot-list mailing list
>>> Soot-list at sable.mcgill.ca
>>> http://mailman.cs.mcgill.ca/mailman/listinfo/soot-list
>> _______________________________________________
>> Soot-list mailing list
>> Soot-list at sable.mcgill.ca
>> http://mailman.cs.mcgill.ca/mailman/listinfo/soot-list
>> 
> _______________________________________________
> Soot-list mailing list
> Soot-list at sable.mcgill.ca
> http://mailman.cs.mcgill.ca/mailman/listinfo/soot-list

--
Eric Bodden, Ph.D., http://sse.ec-spride.de/ http://bodden.de/
Head of Secure Software Engineering Group at EC SPRIDE
Tel: +49 6151 16-75422    Fax: +49 6151 16-72051
Room 3.2.14, Mornewegstr. 30, 64293 Darmstadt