Differences

This shows you the differences between two versions of the page.

Link to this comparison view

Both sides previous revisionPrevious revision
Next revision		Previous revision
research:software:secdart [2017/05/26 21:05] – racruzresearch:software:secdart [2017/12/05 14:05] (current) – [Dart subset] racruz
Line 1: Line 1:
 ====== Gradual Security Typing in Dart ====== ====== Gradual Security Typing in Dart ======
 This page will describe artifacts associated to SecDart which is an extension to the Dart programming language with gradual security typing. This page will describe artifacts associated to SecDart which is an extension to the Dart programming language with gradual security typing.
 +
 +===== Installation instructions =====
 +We will provide three ways to interact with the SecDart's security analysis (currently just the first one is available!): 
 +  * **Using the online SecDart Pad** at [[https://pleiad.cl/secdart/|https://pleiad.cl/secdart/]]
 +  * **The SecDart Analyzer CLI**
 +  * **The SecDart Plugin for Analysis Server**.
 +
 +
 +===== SecDart Pad: Functionality =====
 +The following screenshot shows how the SecDart Pad looks like
 +
 +{{:research:software:secdart:example_1.png?nolink&600|}}
 +
 +===== The SecDart Analyzer CLI =====
 +//Instructions will be placed here soon.//
 +
  
 ===== Integration with the Analysis Server ===== ===== Integration with the Analysis Server =====
 We developed a plugin for the [[https://github.com/dart-lang/sdk/tree/master/pkg/analysis_server|Dart Analysis Server]]. The implementation is not stable yet, but we are working on that. The following screenshot shows a (custom) security error reported by the security analysis in the "Dart Analysis" windows of WebStorm We developed a plugin for the [[https://github.com/dart-lang/sdk/tree/master/pkg/analysis_server|Dart Analysis Server]]. The implementation is not stable yet, but we are working on that. The following screenshot shows a (custom) security error reported by the security analysis in the "Dart Analysis" windows of WebStorm
  
-{{:research:software:secdart:implict_flows.png?1000|}}+{{:research:software:secdart:implict_flows.png?600|}} 
 + 
 +===== SecDart : Language features ===== 
 +SecDart covers a subset of the language and add security labels to language constructors 
 + 
 +==== Dart subset ==== 
 +The following BNF notation represents the AST of the supported subset of Dart, so is not a grammar specification. We use brackets in the BNF rules to refer to the name of the class of the Ast node provided by the Dart Analyzer. 
 + 
 +<code> 
 + compilationUnitMember ::=  
 +       | [FunctionDeclaration] 
 +   
 + functionDeclaration ::= 
 +         'external' functionSignature 
 +       | functionSignature [FunctionBody] 
 +  
 + functionSignature ::= 
 +         [Type]? ('get' | 'set')? [SimpleIdentifier] [FormalParameterList] 
 +          
 + binaryExpression ::= 
 +        [Expression] [Token] [Expression]  
 +  
 +          
 + functionBody ::= 
 +         [BlockFunctionBody] 
 +       | [EmptyFunctionBody] 
 +       | [ExpressionFunctionBody] 
 +        
 + blockFunctionBody ::= block 
 + 
 + expressionFunctionBody ::= '=>' [Expression] ';' 
 + 
 + block ::= '{' statement* '} 
 + 
 + statement ::= 
 +         [Block] 
 +       | [VariableDeclarationStatement] 
 +       | [IfStatement] 
 +       | [ReturnStatement] 
 +       | [ExpressionStatement]  
 +        
 + variableDeclarationStatement ::=  
 +         [VariableDeclarationList] ';' 
 +          
 + variableDeclarationList ::= 
 +         finalConstVarOrType [VariableDeclaration] (',' [VariableDeclaration])* 
 +          
 + variableDeclaration ::= 
 +         [SimpleIdentifier] ('=' [Expression])? 
 +          
 + ifStatement ::= 
 +         'if' '(' [Expression] ')' [Statement] ('else' [Statement])? 
 +          
 + returnStatement ::= 
 +         'return' [Expression]? ';' 
 +          
 + expressionStatement ::= 
 +         [Expression]? ';' 
 + 
  
 + expression ::=
 +         [AssignmentExpression]
 +       | [ConditionalExpression] cascadeSection*
 +       //the Dart grammar does not include the followings nodes here to avoid left recursion, however for the sake of presentation we inline them here.
 +       | [BinaryExpression]
 +       | [InvocationExpression]
 +       | [Literal]
 +       | [ParenthesizedExpression]
 +       | [Identifier]
 +       
 + assignmentExpression ::=
 +         [Expression] assignmentOperator [Expression]
 +         
 + conditionalExpression ::=
 +         [Expression] '?' [Expression] ':' [Expression]      
 +</code>
 +==== Security labels ====
 +SecDart uses annotations to specify security labels. We can specify security labels for the following entities:
 +  * parameters of functions <code>
 +int min(@high int a,@high int b)
 +</code>
 +  * variable definition <code>
 +void sendToFacebook(){
 +   ...
 +   @low String message = ....
 +   ...
 +}
 +</code>
 +  * function declarations <code>
 +@latent("H","H")
 +@low int max(@low int a,@high int b){
 +   return a+b;
 +}
 +</code>