dangtunguyen / iotsan Goto Github PK

IotSan: Fortifying the Safety of IoT Systems (ACM CoNEXT'18)

License: Other

Groovy 4.80% Java 21.46% Batchfile 0.03% Shell 0.06% HTML 73.39% JavaScript 0.01% CSS 0.10% ANTLR 0.03% GAP 0.12% Smarty 0.01%

security privacy formal-verification model-checking iot translator static-code-analysis

iotsan's Introduction

Overview

In this repository you will find the detailed technical report and protype code of IoTSan, a model-checking-based tool used to verify the safety of IoT systems.

This work is published at The 14th International Conference on emerging Networking EXperiments and Technologies (CoNEXT '18).

Code Structure

IoTSan is developed based on Bandera and its code structure is as following:

The "App Dependency Analyzer" module and "Translator" (Groovy to Java) module are at "IoTSan/src/edu/ksu/cis/bandera/jjjc/gparser/"
The "Model Generator" module is at "IoTSan/src/edu/ksu/cis/bandera/spin/"
The "Configuration Extractor" module is at "IoTSan/src/configextractor" (This module is not yet integrated into IoTSan at this initial version).

Note: This is the initial version of IoTSan, which does not include all of the modules mentioned in the paper. I will update this repository with additional modules.

Using The Tool

Create an Eclipse project and clone this repository (you can find the instructions here).
Make sure to include all the files (e.g., Lexer.data) in your project.
Install Groovy plugin on Eclipse following the instructions at here
Add all libraries (.jar files) in the "IoTSan/lib" folder.
Create the folder "input/smartapps" at the root directory of your porject. You then need to put the source code of apps and their configuration files in this folder. Note that you should give good names to app files since they will become the names of apps in the resulting modeled system.
Run the "IotSan.java" as "Java Application". The resulting Promela model code will be generated and stored at ".../IoTSan/output/IotSanOutput/birc".
Append the safety property in LTL format to the end of each output file.
Run the verification with SPIN using the following command in a terminal: spin -search -DVECTORSZ=36736 -DSAFETY -DBITSTATE -E -NOBOUNDCHECK -NOFAIR -NOCOMP -n -w36 <Promela file>. For example: spin -search -DVECTORSZ=36736 -DSAFETY -DBITSTATE -E -NOBOUNDCHECK -NOFAIR -NOCOMP -n -w36 SmartThings0.prom
If any violation is detected, the file "SmartThing0.prom.trail" will be created by SPIN. Use the following command to get counter-example log: spin -p -replay SmartThings0.prom > log.txt
Get a filtered logs by using: grep -v 'allEvtsHandled' log.txt | grep -v 'generatedEvent.EvtType = g_' | grep -E 'generatedEvent.EvtType =|ST_Command.EvtType =|BroadcastChans|Handle|assert|location.mode' > filterLog.txt

Note that you need to install SPIN by following instructions here before using this tool.

Samples

Please refer to the directory "IoTSan/samples/" for examples of app source code, config files, and log files.

Here is the snapshot of a verification run:

Citation

If you use the source code, please cite the following paper:

Dang Tu Nguyen, Chengyu Song, Zhiyun Qian, Srikanth V. Krishnamurthy, Edward J. M. Colbert, and Patrick McDaniel, "IotSan: Fortifying the Safety of IoT Systems," In Proc. of the 14th International Conference on emerging Networking EXperiments and Technologies (CoNEXT '18)

iotsan's People

Contributors

Stargazers

Watchers

Forkers

yizhuozhai maxvonhippel beerkay dianakoh clayness quz105 hobama chanyeol525

iotsan's Issues

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!

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

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?

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?

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.