search

mbeddr / mbeddr.core

The mbeddr core. An extensible C
Eclipse Public License 2.0
225 stars 77 forks source link

Robustness Analysis Fails - A Bug In HTML Results Saver #1064

Open qutorial opened 10 years ago

qutorial commented 10 years ago

In the code/applications/HeartBleed on the fortissStable branch running the robustness analyses on Linux generates 36 claims and the defect is detected. On Mac OS X only 12 claims generate and the defect stays unrevealed.

To reproduce: checkout fortissStable branch, open code/applications/HeartBleed, check the first analysis configuration, one claim has to fail. But all succeed. 36 claims have to be there, but only 12 are shown.

qutorial commented 10 years ago

Results saved in: /Users/fortiss/mbeddr/mbeddr.github/code/applications/HeartBleed/solutions/analyses_results/HearBleedImpl/Model1/xmlCBMCRawOutput/HearBleedImpl.Model1_nightly.html java.lang.NullPointerException at com.mbeddr.analyses.cbmc.rt.run.HTMLResultsSaver$1.run(HTMLResultsSaver.java:66) at jetbrains.mps.ide.smodel.WorkbenchModelAccess$2.run(WorkbenchModelAccess.java:116) at com.intellij.openapi.application.impl.ApplicationImpl.runReadAction(ApplicationImpl.java:911) at jetbrains.mps.ide.smodel.WorkbenchModelAccess.runReadAction(WorkbenchModelAccess.java:111) at com.mbeddr.analyses.cbmc.rt.run.HTMLResultsSaver.generateHTMLPage(HTMLResultsSaver.java:63) at com.mbeddr.analyses.cbmc.rt.run.AnalysisConfigurationAnalyzer.doSaveResults(AnalysisConfigurationAnalyzer.java:161) at com.mbeddr.analyses.cbmc.rt.run.AnalysisConfigurationAnalyzer.doInBackground(AnalysisConfigurationAnalyzer.java:100) at com.mbeddr.analyses.cbmc.rt.run.AnalysisConfigurationAnalyzer.doInBackground(AnalysisConfigurationAnalyzer.java:1) at javax.swing.SwingWorker$1.call(SwingWorker.java:277) at java.util.concurrent.FutureTask$Sync.innerRun(FutureTask.java:303) at java.util.concurrent.FutureTask.run(FutureTask.java:138) at javax.swing.SwingWorker.run(SwingWorker.java:316) at java.util.concurrent.ThreadPoolExecutor$Worker.runTask(ThreadPoolExecutor.java:895) at java.util.concurrent.ThreadPoolExecutor$Worker.run(ThreadPoolExecutor.java:918) at java.lang.Thread.run(Thread.java:695)

qutorial commented 10 years ago

Cbmc works fine on it, reporting a problem cbmc HeartBleed.c --bounds-check --pointer-check --function HeartBleed_verification --unwind 30

danielratiu commented 10 years ago

on windows I got 36 results and one claim failed

qutorial commented 10 years ago

Continuing investigation:

1) On Linux and Windows: This is wrong to have 36 claims. They have to be 18. It probably counts from two functions, HeartBleed_verification and HeartBleed_verificationFixed, whereas only one should be taken into account.

2) On Mac: cbmc produces different names for claims. E.g.

instead of something like Is it a compiler option difference? This is a serious problem indeed - different CBMC results mean not configured fully cbmc. Probably CBMC gets the current machine environment into account, whereas the deployment machine environment should count instead. More cbmc options have to be set to fix such things. Maybe taking them from build configuration?
qutorial commented 10 years ago

On mac a total of 24 claims is generated by CBMC, only 12 are shown by mbeddr

qutorial commented 10 years ago

Ok, so it is in the filter claims where things are getting filtered out wrongly.

Why to filter by the call graph, when cbmc accepts the --function property?

danielratiu commented 10 years ago

in the case of analyses starting from a synthethised environment, we do not want to check robustness of that environment (the users would not understand anything since the environments are completely automatic synthethised)

----- Ursprüngliche Mail ----- Von: "qutorial" notifications@github.com An: "mbeddr/mbeddr.core" mbeddr.core@noreply.github.com CC: "danielratiu" ratiu@fortiss.org Gesendet: Freitag, 16. Mai 2014 13:53:26 Betreff: Re: [mbeddr.core] Robustness Analysis Fails - A Bug In HTML Results Saver (#1064)

Ok, so it is in the filter claims where things are getting filtered out wrongly.

Why to filter by the call graph, when cbmc accepts the --function property?

Reply to this email directly or view it on GitHub: https://github.com/mbeddr/mbeddr.core/issues/1064#issuecomment-43323069

qutorial commented 10 years ago

An example?

qutorial commented 10 years ago

I brought back the formerly filtered out __built_in CBMC checks. But it still works differently on MAC, producing just 24 claims. None of them fails (one has to).

qutorial commented 10 years ago

Okay.

The memcpy() related bug is classified as an arithmetic overflow problem by CBMC on Mac, instead of a pointer dereference :(

To reproduce, just get the master, and run the simplest, third analysis configuration.

danielratiu commented 10 years ago

my last answer was slightly wrong: when calling "cbmc --show-properties --function foo file.c", cbmc shows ALL claims from file.c, even if they belong to program parts not reachable from function "foo". So, many checks will be superfluous and results true.

----- Ursprüngliche Mail ----- Von: "qutorial" notifications@github.com An: "mbeddr/mbeddr.core" mbeddr.core@noreply.github.com CC: "danielratiu" ratiu@fortiss.org Gesendet: Freitag, 16. Mai 2014 14:51:09 Betreff: Re: [mbeddr.core] Robustness Analysis Fails - A Bug In HTML Results Saver (#1064)

I brought back the formerly filtered out __built_in CBMC checks. But it still works differently on MAC, producing just 24 claims. None of them fails (one has to).

Reply to this email directly or view it on GitHub: https://github.com/mbeddr/mbeddr.core/issues/1064#issuecomment-43327242

qutorial commented 10 years ago

I guess we should delete the confusing --function XYZ cbmc setting. It has no effect. Right?

qutorial commented 10 years ago

Ok, it returns also false positives, when memcpy() is used.

uint8[10] src; uint8[10] dst; memcpy(dst,src,5); <--- overflow.

Reported as Arithmetic overflow on signed to unsigned conversion.