Skip to content

Commit

Permalink
Fix interaction with idris client
Browse files Browse the repository at this point in the history
The Vim integration was actually vulnerable to
shell injection attacks. This did not yet become
obvious because variables with quotes did not get
sent to the client properly. By fixing this the
attack became possible. I'm using shellescape to
tackle this issue.
  • Loading branch information
raichoo committed Jul 13, 2015
1 parent 4c1723c commit e8563c4
Show file tree
Hide file tree
Showing 2 changed files with 14 additions and 11 deletions.
3 changes: 3 additions & 0 deletions after/ftplugin/idris.vim
Original file line number Diff line number Diff line change
@@ -0,0 +1,3 @@
setlocal comments=s1fl:{-,mb:-,ex:-},:--
setlocal formatoptions-=cro formatoptions+=j
setlocal iskeyword+='
22 changes: 11 additions & 11 deletions ftplugin/idris.vim
Original file line number Diff line number Diff line change
Expand Up @@ -70,7 +70,7 @@ endfunction

function! IdrisReload(q)
w
let file = expand("%:p")
let file = shellescape(expand("%:p"))
let tc = system("idris --client ':l " . file . "'")
if (! (tc is ""))
call IWrite(tc)
Expand All @@ -85,7 +85,7 @@ endfunction

function! IdrisReloadToLine(cline)
w
let file = expand("%:p")
let file = shellescape(expand("%:p"))
let tc = system("idris --client ':lto " . a:cline . " " . file . "'")
if (! (tc is ""))
call IWrite(tc)
Expand All @@ -95,7 +95,7 @@ endfunction

function! IdrisShowType()
w
let word = expand("<cword>")
let word = shellescape(expand("<cword>"))
let cline = line(".")
let tc = IdrisReloadToLine(cline)
if (! (tc is ""))
Expand All @@ -109,7 +109,7 @@ endfunction

function! IdrisShowDoc()
w
let word = expand("<cword>")
let word = shellescape(expand("<cword>"))
let ty = system("idris --client ':doc " . word . "'")
call IWrite(ty)
endfunction
Expand All @@ -118,7 +118,7 @@ function! IdrisProofSearch(hint)
let view = winsaveview()
w
let cline = line(".")
let word = expand("<cword>")
let word = shellescape(expand("<cword>"))
let tc = IdrisReload(1)

if (a:hint==0)
Expand All @@ -143,7 +143,7 @@ function! IdrisMakeLemma()
let view = winsaveview()
w
let cline = line(".")
let word = expand("<cword>")
let word = shellescape(expand("<cword>"))
let tc = IdrisReload(1)

if (tc is "")
Expand All @@ -163,7 +163,7 @@ function! IdrisRefine()
let view = winsaveview()
w
let cline = line(".")
let word = expand("<cword>")
let word = shellescape(expand("<cword>"))
let tc = IdrisReload(1)

let name = input ("Name: ")
Expand All @@ -184,7 +184,7 @@ function! IdrisAddMissing()
let view = winsaveview()
w
let cline = line(".")
let word = expand("<cword>")
let word = shellescape(expand("<cword>"))
let tc = IdrisReload(1)

if (tc is "")
Expand All @@ -203,7 +203,7 @@ function! IdrisCaseSplit()
let view = winsaveview()
w
let cline = line(".")
let word = expand("<cword>")
let word = shellescape(expand("<cword>"))
let tc = IdrisReloadToLine(cline)

if (tc is "")
Expand All @@ -222,7 +222,7 @@ function! IdrisMakeWith()
let view = winsaveview()
w
let cline = line(".")
let word = expand("<cword>")
let word = shellescape(expand("<cword>"))
let tc = IdrisReload(1)

if (tc is "")
Expand All @@ -242,7 +242,7 @@ function! IdrisAddClause(proof)
let view = winsaveview()
w
let cline = line(".")
let word = expand("<cword>")
let word = shellescape(expand("<cword>"))
let tc = IdrisReloadToLine(cline)

if (tc is "")
Expand Down

0 comments on commit e8563c4

Please sign in to comment.