====== 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.

===== 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 =====
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?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>