dangtunguyen / iotsan Goto Github PK
View Code? Open in Web Editor NEWIotSan: Fortifying the Safety of IoT Systems (ACM CoNEXT'18)
License: Other
iotsan's People
Contributors
Stargazers
Watchers
iotsan's Issues
Expected output? (Possible C error)
On the provided input files, I run the project as a Java App and then get back a SmartThings0.prom file as expected. I don't append any additional LTL properties to the file. Then I do the following:
spin -search -DVECTORSZ=36736 -DSAFETY -DBITSTATE -E -NOBOUNDCHECK -NOFAIR -NOCOMP -n -w36 SmartThings0.prom
I get back:
pan.c: In function ‘wrap_stats’:
pan.c:11875:9: warning: too many arguments for format [-Wformat-extra-args]
printf("random seed used: 0\n", (uint) (s_rand-1));
^~~~~~~~~~~~~~~~~~~~~~~
pan.c: In function ‘make_trail’:
pan.c:5851:19: warning: ‘%d’ directive writing between 1 and 10 bytes into a region of size between 1 and 512 [-Wformat-overflow=]
sprintf(fnm, "%s%d.%s",
^~
pan.c:5851:16: note: directive argument in the range [1, 2147483647]
sprintf(fnm, "%s%d.%s",
^~~~~~~~~
In file included from /usr/include/stdio.h:873,
from pan.c:7:
/usr/include/x86_64-linux-gnu/bits/stdio2.h:36:10: note: ‘__builtin___sprintf_chk’ output 3 or more bytes (assuming 523) into a destination of size 512
return __builtin___sprintf_chk (__s, __USE_FORTIFY_LEVEL - 1,
^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
__bos (__s), __fmt, __va_arg_pack ());
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
pan.c:5859:22: warning: ‘__builtin___sprintf_chk’ may write a terminating nul past the end of the destination [-Wformat-overflow=]
sprintf(fnm, "%s.%s", MyFile, tprefix);
^
In file included from /usr/include/stdio.h:873,
from pan.c:7:
/usr/include/x86_64-linux-gnu/bits/stdio2.h:36:10: note: ‘__builtin___sprintf_chk’ output 2 or more bytes (assuming 513) into a destination of size 512
return __builtin___sprintf_chk (__s, __USE_FORTIFY_LEVEL - 1,
^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
__bos (__s), __fmt, __va_arg_pack ());
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
pan.c:5866:21: warning: ‘%d’ directive writing between 1 and 10 bytes into a region of size between 1 and 512 [-Wformat-overflow=]
sprintf(fnm, "%s%d.%s",
^~
pan.c:5866:18: note: directive argument in the range [1, 2147483646]
sprintf(fnm, "%s%d.%s",
^~~~~~~~~
In file included from /usr/include/stdio.h:873,
from pan.c:7:
/usr/include/x86_64-linux-gnu/bits/stdio2.h:36:10: note: ‘__builtin___sprintf_chk’ output 3 or more bytes (assuming 523) into a destination of size 512
return __builtin___sprintf_chk (__s, __USE_FORTIFY_LEVEL - 1,
^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
__bos (__s), __fmt, __va_arg_pack ());
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
pan.c:5869:24: warning: ‘__builtin___sprintf_chk’ may write a terminating nul past the end of the destination [-Wformat-overflow=]
sprintf(fnm, "%s.%s", MyFile, tprefix);
^
In file included from /usr/include/stdio.h:873,
from pan.c:7:
/usr/include/x86_64-linux-gnu/bits/stdio2.h:36:10: note: ‘__builtin___sprintf_chk’ output 2 or more bytes (assuming 513) into a destination of size 512
return __builtin___sprintf_chk (__s, __USE_FORTIFY_LEVEL - 1,
^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
__bos (__s), __fmt, __va_arg_pack ());
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
pan.c: In function ‘findtrail’:
pan.c:5466:22: warning: ‘%s’ directive writing 5 bytes into a region of size between 0 and 511 [-Wformat-overflow=]
pan.c:5438:12:
tprefix = "trail";
~~~~~~~
pan.c:5466:22:
{ sprintf(fnm, "%s.%s", MyFile, tprefix);
^~
In file included from /usr/include/stdio.h:873,
from pan.c:7:
/usr/include/x86_64-linux-gnu/bits/stdio2.h:36:10: note: ‘__builtin___sprintf_chk’ output between 7 and 518 bytes into a destination of size 512
return __builtin___sprintf_chk (__s, __USE_FORTIFY_LEVEL - 1,
^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
__bos (__s), __fmt, __va_arg_pack ());
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
pan.c:5477:24: warning: ‘__builtin___sprintf_chk’ may write a terminating nul past the end of the destination [-Wformat-overflow=]
sprintf(fnm, "%s.%s", MyFile, tprefix);
^
In file included from /usr/include/stdio.h:873,
from pan.c:7:
/usr/include/x86_64-linux-gnu/bits/stdio2.h:36:10: note: ‘__builtin___sprintf_chk’ output 2 or more bytes (assuming 513) into a destination of size 512
return __builtin___sprintf_chk (__s, __USE_FORTIFY_LEVEL - 1,
^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
__bos (__s), __fmt, __va_arg_pack ());
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
pan.c:5442:23: warning: ‘.’ directive writing 1 byte into a region of size between 0 and 511 [-Wformat-overflow=]
{ sprintf(fnm, "%s%d.%s",
^
In file included from /usr/include/stdio.h:873,
from pan.c:7:
/usr/include/x86_64-linux-gnu/bits/stdio2.h:36:10: note: ‘__builtin___sprintf_chk’ output between 8 and 529 bytes into a destination of size 512
return __builtin___sprintf_chk (__s, __USE_FORTIFY_LEVEL - 1,
^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
__bos (__s), __fmt, __va_arg_pack ());
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
pan.c:5454:23: warning: ‘.’ directive writing 1 byte into a region of size between 0 and 511 [-Wformat-overflow=]
sprintf(fnm, "%s%d.%s",
^
In file included from /usr/include/stdio.h:873,
from pan.c:7:
/usr/include/x86_64-linux-gnu/bits/stdio2.h:36:10: note: ‘__builtin___sprintf_chk’ output 3 or more bytes (assuming 514) into a destination of size 512
return __builtin___sprintf_chk (__s, __USE_FORTIFY_LEVEL - 1,
^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
__bos (__s), __fmt, __va_arg_pack ());
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
pan.c:5516:21: warning: ‘%s’ directive writing 5 bytes into a region of size between 0 and 511 [-Wformat-overflow=]
pan.c:5503:12:
tprefix = "trail";
~~~~~~~
pan.c:5516:21:
{ sprintf(fnm, "%s.%s", MyFile, tprefix);
^~
In file included from /usr/include/stdio.h:873,
from pan.c:7:
/usr/include/x86_64-linux-gnu/bits/stdio2.h:36:10: note: ‘__builtin___sprintf_chk’ output between 7 and 518 bytes into a destination of size 512
return __builtin___sprintf_chk (__s, __USE_FORTIFY_LEVEL - 1,
^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
__bos (__s), __fmt, __va_arg_pack ());
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
pan.c:5520:23: warning: ‘__builtin___sprintf_chk’ may write a terminating nul past the end of the destination [-Wformat-overflow=]
sprintf(fnm, "%s.%s", MyFile, tprefix);
^
In file included from /usr/include/stdio.h:873,
from pan.c:7:
/usr/include/x86_64-linux-gnu/bits/stdio2.h:36:10: note: ‘__builtin___sprintf_chk’ output 2 or more bytes (assuming 513) into a destination of size 512
return __builtin___sprintf_chk (__s, __USE_FORTIFY_LEVEL - 1,
^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
__bos (__s), __fmt, __va_arg_pack ());
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
pan.c:5506:22: warning: ‘.’ directive writing 1 byte into a region of size between 0 and 511 [-Wformat-overflow=]
{ sprintf(fnm, "%s%d.%s", MyFile, whichtrail, tprefix);
^
In file included from /usr/include/stdio.h:873,
from pan.c:7:
/usr/include/x86_64-linux-gnu/bits/stdio2.h:36:10: note: ‘__builtin___sprintf_chk’ output between 8 and 529 bytes into a destination of size 512
return __builtin___sprintf_chk (__s, __USE_FORTIFY_LEVEL - 1,
^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
__bos (__s), __fmt, __va_arg_pack ());
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
pan.c:5510:22: warning: ‘.’ directive writing 1 byte into a region of size between 0 and 511 [-Wformat-overflow=]
sprintf(fnm, "%s%d.%s",
^
In file included from /usr/include/stdio.h:873,
from pan.c:7:
/usr/include/x86_64-linux-gnu/bits/stdio2.h:36:10: note: ‘__builtin___sprintf_chk’ output 3 or more bytes (assuming 514) into a destination of size 512
return __builtin___sprintf_chk (__s, __USE_FORTIFY_LEVEL - 1,
^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
__bos (__s), __fmt, __va_arg_pack ());
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
warning: only one claim defined, -N ignored
warning: only one claim defined, -N ignored
warning: only one claim defined, -N ignored
(Spin Version 6.4.6 -- 2 December 2016)
+ Partial Order Reduction
Bit statespace search for:
never claim - (none specified)
assertion violations +
cycle checks - (disabled by -DSAFETY)
invalid end states - (disabled by -E flag)
State-vector 10920 byte, depth reached 1753, errors: 0
659442 states, stored
3150 states, matched
662592 transitions (= stored+matched)
496053 atomic steps
hash factor: 104209 (best if > 100.)
bits set per state: 3 (-k3)
Stats on memory usage (in Megabytes):
6880.088 equivalent memory usage for states (stored*(State-vector + overhead))
8192.000 memory used for hash array (-w36)
0.076 memory used for bit stack
0.534 memory used for DFS stack (-m10000)
10.921 other (proc and chan stacks)
2.482 memory lost to fragmentation
8206.014 total actual memory usage
pan: elapsed time 12.4 seconds
pan: rate 53266.721 states/second
Right away, I notice the error or warning or whatever appears to be similar to the one shown in the screenshot in the README. Then, still following the directions, I run:
spin -p -replay SmartThings0.prom > log.txt
The log file is massive, and looks like this:
using statement merging
spin: trail ends after -4 steps
#processes: 1
doorLock_STLock = 0
tomPresence_STPresSensor = 0
frontDoorSensor_STMotionSensor = 0
livingRoomBulb_STSwitch = 0
bedRoomBulb_STSwitch = 0
livingRoomSensor_STMotionSensor = 0
bedRoomSensor_STMotionSensor = 0
bedRoomDoor_STContactSensor = 0
_g_STLockArr.length = 0
_g_STLockArr.element[0].id = 0
_g_STLockArr.element[0].gArrIndex = 0
_g_STLockArr.element[0].events.length = 0
_g_STLockArr.element[0].events.element[0].name = 0
_g_STLockArr.element[0].events.element[0].value = 0
_g_STLockArr.element[0].events.element[0].physical = 0
_g_STLockArr.element[0].events.element[0].deviceId = 0
_g_STLockArr.element[0].events.element[0].date = 0
_g_STLockArr.element[0].events.element[0].id = 0
_g_STLockArr.element[0].events.element[0].unit = 0
_g_STLockArr.element[0].events.element[0].type = 0
_g_STLockArr.element[0].events.element[0].isAlive = 0
_g_STLockArr.element[0].events.element[0].EvtType = 0
_g_STLockArr.element[0].events.element[1].name = 0
_g_STLockArr.element[0].events.element[1].value = 0
_g_STLockArr.element[0].events.element[1].physical = 0
_g_STLockArr.element[0].events.element[1].deviceId = 0
_g_STLockArr.element[0].events.element[1].date = 0
etc etc etc
Next, still following the directions, I run:
grep -v 'allEvtsHandled' log.txt | grep -v 'generatedEvent.EvtType = g_' | grep -E 'generatedEvent.EvtType =|ST_Command.EvtType =|BroadcastChans|Handle|assert|location.mode' > filterLog.txt
I end up with 978 lines of what looks like code:
_g_STLockArr.element[0].BroadcastChans[0] = 0
_g_STLockArr.element[0].BroadcastChans[1] = 0
_g_STLockArr.element[0].BroadcastChans[2] = 0
_g_STLockArr.element[0].BroadcastChans[3] = 0
_g_STLockArr.element[0].BroadcastChans[4] = 0
_g_STLockArr.element[0].BroadcastChans[5] = 0
_g_STLockArr.element[0].BroadcastChans[6] = 0
_g_STLockArr.element[0].BroadcastChans[7] = 0
_g_STLockArr.element[0].BroadcastChans[8] = 0
_g_STLockArr.element[0].BroadcastChans[9] = 0
_g_STLockArr.element[1].BroadcastChans[0] = 0
_g_STLockArr.element[1].BroadcastChans[1] = 0
_g_STLockArr.element[1].BroadcastChans[2] = 0
_g_STLockArr.element[1].BroadcastChans[3] = 0
_g_STLockArr.element[1].BroadcastChans[4] = 0
_g_STLockArr.element[1].BroadcastChans[5] = 0
etc etc etc
My best guess
.... is that an error was thrown in the process of compiling the c code with Spin, which has something to do with that line of code that is shown as erroneous in the screenshot and also shown in the errors I showed above. As a result, this trail file didn't come out as expected, so the logs didn't come out as expected, so I ended up with garbage output.
Question:
Do you have any recommendations/ideas for how to fix my code/setup/dependencies/etc. so that Spin successfully runs the specification output?
How to configure build path?
I'm trying to run the code but am having a lot of trouble with the build path. Do you have any advice for how to correctly configure this?
Thanks,
Max
GTryCatchStmtTransformer mishandled nested try-and-catch statements
I don't know if this is an intentional failure or it's logically sound.
When I tried the following groovy code:
import java.math.BigDecimal
import java.util.Date
import java.util.List
import java.util.Map
import java.util.TimeZone
public class Hello
{
double now() {
try{
try{
System.out.println("Hello World");
}
catch(e){
}
}
catch(e){
}
}
}
By using the following in Java:
GTryCatchStmtTransformer gtcst = new GTryCatchStmtTransformer();
gtcst.processAClassNode(classNode);
In the document of GTryCatchStmtTransformer.java, it says that it will transform
try {
runIn(60*minutes,changeIntensity,[overwrite: false])
}
catch(e)
{
log.debug e
}
into
runIn(60*minutes,changeIntensity,[overwrite: false])
.
However, when I applied process a class node, it turns out the try and catch statement still exists.
My modification towards the code is that I decremented i once we are in a try-and-catch case. But I still wonder if we need to consider to peel the try-and-catch statement all the way in or should we just leave out and peel only the outer most try-and-catch statement?
Best,
Zach
Problem regarding the Java Compilation
It is an excellent paper to read. However, I have some difficulties in compiling the Java code. When I used Eclipse 2020-06 (4.16.0), I could not compile it. It gives me this error:
The type java.lang.StringBuilder cannot be resolved. It is indirectly referenced from required .class files
When I run it as a Java Application, it gives me this error:
java.lang.NoClassDefFoundError: edu/ksu/cis/bandera/bui/AboutBox
Exception in thread "main"
Could you help with me to solve these?
examples of the safety properties
Hello @dangtunguyen,
Thanks for this excellent project and paper! (: I have been looking into systems that assert safety properties in IoT recently, and yours is the only publicly available system that I found.
What do the safety properties look like? I've seen the two samples in the github repository, but I wonder if you are able to make the other safety properties you described in your paper available.
Thanks!
What is `lexer.dat` and how do I make one?
I am having a problem with this line in Lexer.java:
int length = s.readInt();
I am getting the error:
Unable to read lexer.dat
And the error is thrown from that line, when I check using the stacktrace.
Can you please explain what this lexer.dat file is? My best guess is that I need to generate my own lexer.dat file based off of the classes in the files I want to look at, and that this is where the problem lies. My full stack trace is below. My line numbers differ a bit from yours due to comments and minor changes but everything in my version is functionally the same. DPM is just my private wrapper which is calling the IoTSan logic.
Parsing...
java.io.IOException: Stream closed
at java.io.BufferedInputStream.getInIfOpen(BufferedInputStream.java:159)
at java.io.BufferedInputStream.fill(BufferedInputStream.java:246)
at java.io.BufferedInputStream.read(BufferedInputStream.java:265)
at java.io.DataInputStream.readInt(DataInputStream.java:387)
at edu.ksu.cis.bandera.jjjc.unicodepreprocessor.lexer.Lexer.(Lexer.java:111)
at edu.ksu.cis.bandera.jjjc.unicodepreprocessor.UnicodeLexer.(UnicodeLexer.java:48)
at edu.ksu.cis.bandera.jjjc.unicodepreprocessor.UnicodePreprocessor.(UnicodePreprocessor.java:84)
at edu.ksu.cis.bandera.jjjc.CompilationManager.parseFile(CompilationManager.java:745)
at edu.ksu.cis.bandera.jjjc.CompilationManager.compile(CompilationManager.java:423)
at edu.ksu.cis.bandera.jjjc.CompilationManager.compile(CompilationManager.java:373)
at edu.ksu.cis.bandera.bui.GDriver.runJJJC(GDriver.java:439)
at edu.ksu.cis.bandera.bui.GDriver.run(GDriver.java:278)
at DPM.main.java.DPM.App.main(App.java:24)
java.lang.RuntimeException: Unable to read lexer.dat.
at edu.ksu.cis.bandera.jjjc.unicodepreprocessor.lexer.Lexer.(Lexer.java:148)
at edu.ksu.cis.bandera.jjjc.unicodepreprocessor.UnicodeLexer.(UnicodeLexer.java:48)
at edu.ksu.cis.bandera.jjjc.unicodepreprocessor.UnicodePreprocessor.(UnicodePreprocessor.java:84)
at edu.ksu.cis.bandera.jjjc.CompilationManager.parseFile(CompilationManager.java:745)
at edu.ksu.cis.bandera.jjjc.CompilationManager.compile(CompilationManager.java:423)
at edu.ksu.cis.bandera.jjjc.CompilationManager.compile(CompilationManager.java:373)
at edu.ksu.cis.bandera.bui.GDriver.runJJJC(GDriver.java:439)
at edu.ksu.cis.bandera.bui.GDriver.run(GDriver.java:278)
at DPM.main.java.DPM.App.main(App.java:24)
[compile] java.lang.RuntimeException: Unable to read lexer.dat.
Thank you very much for your help!
Recommend Projects
-
React
A declarative, efficient, and flexible JavaScript library for building user interfaces.
-
Vue.js
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
-
Typescript
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
-
TensorFlow
An Open Source Machine Learning Framework for Everyone
-
Django
The Web framework for perfectionists with deadlines.
-
Laravel
A PHP framework for web artisans
-
D3
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
-
Recommend Topics
-
javascript
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
-
web
Some thing interesting about web. New door for the world.
-
server
A server is a program made to process requests and deliver data to clients.
-
Machine learning
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
-
Visualization
Some thing interesting about visualization, use data art
-
Game
Some thing interesting about game, make everyone happy.
Recommend Org
-
Facebook
We are working to build community through open source technology. NB: members must have two-factor auth.
-
Microsoft
Open source projects and samples from Microsoft.
-
Google
Google ❤️ Open Source for everyone.
-
Alibaba
Alibaba Open Source for everyone
-
D3
Data-Driven Documents codes.
-
Tencent
China tencent open source team.