1234:
1788:
43:
1808:
1798:
1123:
743:, or because they may never return an incorrect answer but may also never terminate. Despite these limitations, static analysis can still be valuable: the first type of mechanism might reduce the number of vulnerabilities, while the second can sometimes provide strong assurance of the absence of certain classes of vulnerabilities.
969:
subset. Generally, finding a slice is an unsolvable problem, but by specifying the target behavior subset by the values of a set of variables, it is possible to obtain approximate slices using a data-flow algorithm. These slices are usually used by developers during debugging to locate the source of errors.
949:
Program monitoring records and logs different kinds of information about the program such as resource usage, events, and interactions, so that it can be reviewed to find or pinpoint causes of abnormal behavior. Furthermore, it can be used to perform security audits. Automated monitoring of programs
936:
Software should be tested to ensure its quality and that it performs as it is supposed to in a reliable manner, and that it won’t create conflicts with other software that may function alongside it. The tests are performed by executing the program with an input and evaluating its behavior and the
757:
A third-party optimization tool may be implemented in such a way as to never produce an incorrect optimization, but also so that it can, in some situations, continue running indefinitely until it finds one (which may never happen). In this case, the developer using the tool would have to stop the
968:
For a given subset of a program’s behavior, program slicing consists of reducing the program to the minimum form that still produces the selected behavior. The reduced program is called a “slice” and is a faithful representation of the original program within the domain of the specified behavior
903:(which in this context means a formal model of a piece of code, though in other contexts it can be a model of a piece of hardware) complies with a given specification. Due to the inherent finite-state nature of code, and both the specification and the code being convertible into
821:
Abstract interpretation allows the extraction of information about a possible execution of a program without actually executing the program. This information can be used by compilers to look for possible optimizations or for certifying a program against certain classes of bugs.
727:
In the context of program correctness, static analysis can discover vulnerabilities during the development phase of the program. These vulnerabilities are easier to correct than the ones found during the testing phase since static analysis leads to the root of the vulnerability.
803:, which consists of considering all variables that contain user-supplied data – which is considered "tainted", i.e. insecure – and preventing those variables from being used until they have been sanitized. This technique is often used to prevent
921:
Dynamic analysis can use runtime knowledge of the program to increase the precision of the analysis, while also providing runtime protection, but it can only analyze a single execution of the problem and might degrade the program’s performance due to the runtime checks.
798:
Data-flow analysis is a technique designed to gather information about the values at each point of the program and how they change over time. This technique is often used by compilers to optimize the code. One of the most well known examples of data-flow analysis is
851:. Type checking can also help prevent vulnerabilities by ensuring that a signed value isn't attributed to an unsigned variable. Type checking can be done statically (at compile time), dynamically (at runtime) or a combination of both.
766:. An optimizing compiler is at liberty to generate code that does anything at runtime – even crashes – if it encounters source code whose semantics are unspecified by the language standard in use.
876:
Effect systems are formal systems designed to represent the effects that executing a function or method can have. An effect codifies what is being done and with what it is being done – usually referred to as
784:(CFG) where the nodes are instructions of the program and the edges represent the flow of control. By identifying code blocks and loops a CFG becomes a starting point for compiler-made optimizations.
1035:
Jovanovic, N., Kruegel, C., & Kirda, E. (2006, May). Pixy: A static analysis tool for detecting web application vulnerabilities. In
Security and Privacy, 2006 IEEE Symposium on (pp. 6-pp). IEEE.
780:
The purpose of control-flow analysis is to obtain information about which functions can be called at various points during the execution of a program. The collected information is represented by a
694:
is the process of automatically analyzing the behavior of computer programs regarding a property such as correctness, robustness, safety and liveness. Program analysis focuses on two major areas:
836:
Type systems associate types to programs that fulfill certain requirements. Their purpose is to select a subset of programs of a language that are considered correct according to a property.
941:
should be performed to ensure that an attacker can’t tamper with the software and steal information, disrupt the software’s normal operations, or use it as a pivot to attack its users.
673:
702:. The first focuses on improving the program’s performance while reducing the resource usage while the latter focuses on ensuring that the program does what it is supposed to do.
627:
746:
Incorrect optimizations are highly undesirable. So, in the context of program optimization, there are two main strategies to handle computationally undecidable analysis:
594:
754:, may use a truncated version of an analysis that is guaranteed to complete in a finite amount of time, and guaranteed to only find correct optimizations.
1155:
666:
436:
584:
1080:
659:
559:
300:
579:
740:
736:
617:
1233:
526:
290:
847:
Type checking is used in programming to limit how programming objects are used and what can they do. This is done by the compiler or
1410:
393:
126:
60:
31:
1107:
993:
516:
511:
267:
1509:
645:
107:
762:
However, there is also a third strategy that is sometimes applicable for languages that are not completely specified, such as
1670:
1524:
1218:
1183:
536:
249:
229:
79:
64:
1063:
Chunlei, Wang; Gang, Zhao; Yiqi, Dai (2009). "An
Efficient Control Flow Security Analysis Approach for Binary Executables".
1760:
446:
335:
325:
275:
858:, or explicitly provided by type annotations in the source code) can also be used to do optimizations, such as replacing
1723:
1242:
1193:
758:
tool and avoid running the tool on that piece of code again (or possibly modify the code to avoid tripping up the tool).
622:
350:
315:
166:
86:
1698:
1617:
441:
413:
1127:
1148:
1728:
1448:
564:
408:
295:
285:
224:
1811:
93:
53:
1832:
1801:
1791:
1319:
1141:
330:
310:
1642:
1440:
916:
763:
735:, the mechanisms for performing it may not always terminate with the correct answer. This can result in either
710:
471:
340:
320:
1373:
1050:
75:
1602:
1358:
1350:
983:
848:
816:
750:
An optimizer that is expected to complete in a relatively short amount of time, such as the optimizer in an
722:
706:
599:
481:
360:
234:
1745:
1740:
1543:
1262:
541:
451:
403:
345:
1571:
1470:
1368:
1274:
1267:
978:
907:, it is possible to check if the system violates the specification using efficient algorithmic methods.
775:
398:
365:
181:
171:
1538:
1533:
1420:
1296:
1284:
1213:
1003:
998:
951:
695:
461:
305:
239:
206:
186:
147:
1453:
1550:
1385:
1257:
751:
732:
699:
456:
375:
201:
1519:
1460:
1430:
1415:
1380:
1279:
1223:
1178:
1099:
1086:
793:
781:
574:
1634:
1208:
1076:
100:
1581:
1480:
1405:
1314:
1068:
938:
931:
687:
531:
494:
476:
466:
191:
1685:
1475:
1395:
1304:
963:
904:
418:
370:
254:
176:
1703:
1662:
1586:
1514:
1494:
1400:
1363:
1329:
1198:
894:
855:
800:
1826:
1390:
1324:
1188:
1065:
2009 2nd IEEE International
Conference on Computer Science and Information Technology
871:
804:
161:
1090:
1750:
1733:
1576:
1203:
988:
244:
1023:
17:
1566:
1425:
1072:
840:
831:
42:
1652:
1647:
859:
1713:
1529:
1309:
937:
produced output. Even if no security requirements are specified, additional
196:
1122:
899:
Model checking refers to strict, formal, and automated ways to check if a
1612:
569:
521:
506:
501:
1607:
1465:
280:
1675:
1133:
1765:
1755:
355:
705:
Program analysis can be performed without executing the program (
1718:
1693:
739:("no problems found" when the code does in fact have issues) or
589:
1137:
807:
attacks. Taint checking can be done statically or dynamically.
36:
843:– verify whether the program is accepted by the type system.
1708:
731:
Due to many forms of static analysis being computationally
1022:
Nielson, F., Nielson, H. R., & Hankin, C. (2015).
1684:
1661:
1633:
1626:
1595:
1559:
1502:
1493:
1439:
1349:
1342:
1295:
1250:
1241:
1171:
67:. Unsourced material may be challenged and removed.
27:Process of analyzing computer program behavior
1149:
667:
8:
1807:
1797:
1630:
1499:
1346:
1247:
1156:
1142:
1134:
674:
660:
138:
127:Learn how and when to remove this message
1015:
146:
628:Electrical and electronics engineering
7:
1049:Agrawal, Hiralal; Horgan, Joseph R.
65:adding citations to reliable sources
25:
554:Standards and bodies of knowledge
32:Program analysis (disambiguation)
1806:
1796:
1787:
1786:
1232:
1121:
994:Profiling (computer programming)
854:Static type information (either
41:
1108:Springer Science+Business Media
713:) or in a combination of both.
646:Outline of software development
52:needs additional citations for
1104:Principles of Program Analysis
1024:Principles of program analysis
1:
950:is sometimes referred to as
1510:Curry–Howard correspondence
1073:10.1109/ICCSIT.2009.5234950
1849:
961:
929:
914:
892:
869:
829:
814:
791:
773:
720:
409:Software quality assurance
29:
1782:
1230:
1102:; Hankin, Chris (2005).
917:Dynamic program analysis
911:Dynamic program analysis
711:dynamic program analysis
394:Configuration management
1359:Abstract interpretation
1052:Dynamic program slicing
984:Language-based security
817:Abstract interpretation
811:Abstract interpretation
723:Static program analysis
717:Static program analysis
707:static program analysis
618:Artificial intelligence
542:Infrastructure as code
388:Supporting disciplines
1268:Categorical semantics
979:Automated code review
862:with unboxed arrays.
776:Control-flow analysis
399:Deployment management
1214:Runtime verification
1130:at Wikimedia Commons
1067:. pp. 272–276.
1004:Termination analysis
999:Program verification
952:runtime verification
696:program optimization
219:Paradigms and models
148:Software development
61:improve this article
30:For other uses, see
1471:Invariant inference
1219:Safety and liveness
1100:Nielson, Hanne Riis
1098:Nielson, Flemming;
752:optimizing compiler
709:), during runtime (
700:program correctness
142:Part of a series on
1635:Constraint solvers
1461:Concolic execution
1416:Symbolic execution
1224:Undefined behavior
1179:Control-flow graph
794:Data-flow analysis
788:Data-flow analysis
782:control-flow graph
537:Release automation
414:Project management
76:"Program analysis"
1820:
1819:
1778:
1777:
1774:
1773:
1489:
1488:
1338:
1337:
1126:Media related to
1082:978-1-4244-4519-6
684:
683:
575:ISO/IEC standards
137:
136:
129:
111:
18:Software analysis
16:(Redirected from
1840:
1833:Program analysis
1810:
1809:
1800:
1799:
1790:
1789:
1686:Proof assistants
1631:
1500:
1347:
1320:Rewriting system
1315:Process calculus
1248:
1236:
1165:Program analysis
1158:
1151:
1144:
1135:
1128:Program analysis
1125:
1111:
1094:
1059:
1057:
1036:
1033:
1027:
1020:
939:security testing
932:Software testing
905:logical formulae
885:, respectively.
692:program analysis
688:computer science
676:
669:
662:
623:Computer science
532:Build automation
139:
132:
125:
121:
118:
112:
110:
69:
45:
37:
21:
1848:
1847:
1843:
1842:
1841:
1839:
1838:
1837:
1823:
1822:
1821:
1816:
1770:
1680:
1657:
1622:
1596:Data structures
1591:
1555:
1485:
1476:Program slicing
1435:
1334:
1305:Lambda calculus
1291:
1237:
1228:
1189:Hyperproperties
1167:
1162:
1118:
1097:
1083:
1062:
1055:
1048:
1045:
1043:Further reading
1040:
1039:
1034:
1030:
1021:
1017:
1012:
975:
966:
964:Program slicing
960:
958:Program slicing
947:
934:
928:
919:
913:
897:
891:
874:
868:
834:
828:
819:
813:
796:
790:
778:
772:
741:false positives
737:false negatives
725:
719:
680:
651:
650:
641:
633:
632:
613:
605:
604:
555:
547:
546:
497:
487:
486:
432:
424:
423:
419:User experience
389:
381:
380:
271:
260:
259:
220:
212:
211:
157:
156:Core activities
133:
122:
116:
113:
70:
68:
58:
46:
35:
28:
23:
22:
15:
12:
11:
5:
1846:
1844:
1836:
1835:
1825:
1824:
1818:
1817:
1815:
1814:
1804:
1794:
1783:
1780:
1779:
1776:
1775:
1772:
1771:
1769:
1768:
1763:
1758:
1753:
1748:
1743:
1738:
1737:
1736:
1726:
1721:
1716:
1711:
1706:
1701:
1696:
1690:
1688:
1682:
1681:
1679:
1678:
1673:
1667:
1665:
1659:
1658:
1656:
1655:
1650:
1645:
1639:
1637:
1628:
1624:
1623:
1621:
1620:
1615:
1610:
1605:
1599:
1597:
1593:
1592:
1590:
1589:
1584:
1579:
1574:
1569:
1563:
1561:
1557:
1556:
1554:
1553:
1548:
1547:
1546:
1536:
1527:
1522:
1517:
1515:Loop invariant
1512:
1506:
1504:
1497:
1495:Formal methods
1491:
1490:
1487:
1486:
1484:
1483:
1478:
1473:
1468:
1463:
1458:
1457:
1456:
1454:Taint tracking
1445:
1443:
1437:
1436:
1434:
1433:
1428:
1423:
1418:
1413:
1408:
1403:
1401:Model checking
1398:
1393:
1388:
1383:
1378:
1377:
1376:
1366:
1361:
1355:
1353:
1344:
1340:
1339:
1336:
1335:
1333:
1332:
1330:Turing machine
1327:
1322:
1317:
1312:
1307:
1301:
1299:
1293:
1292:
1290:
1289:
1288:
1287:
1282:
1272:
1271:
1270:
1260:
1254:
1252:
1245:
1239:
1238:
1231:
1229:
1227:
1226:
1221:
1216:
1211:
1209:Rice's theorem
1206:
1201:
1199:Path explosion
1196:
1191:
1186:
1181:
1175:
1173:
1169:
1168:
1163:
1161:
1160:
1153:
1146:
1138:
1132:
1131:
1117:
1116:External links
1114:
1113:
1112:
1095:
1081:
1060:
1044:
1041:
1038:
1037:
1028:
1014:
1013:
1011:
1008:
1007:
1006:
1001:
996:
991:
986:
981:
974:
971:
962:Main article:
959:
956:
946:
943:
930:Main article:
927:
924:
915:Main article:
912:
909:
895:Model checking
893:Main article:
890:
889:Model checking
887:
870:Main article:
867:
866:Effect systems
864:
845:
844:
830:Main article:
827:
824:
815:Main article:
812:
809:
801:taint checking
792:Main article:
789:
786:
774:Main article:
771:
768:
760:
759:
755:
721:Main article:
718:
715:
682:
681:
679:
678:
671:
664:
656:
653:
652:
649:
648:
642:
639:
638:
635:
634:
631:
630:
625:
620:
614:
611:
610:
607:
606:
603:
602:
597:
592:
587:
582:
577:
572:
567:
565:IEEE standards
562:
556:
553:
552:
549:
548:
545:
544:
539:
534:
529:
524:
519:
514:
509:
504:
498:
493:
492:
489:
488:
485:
484:
479:
474:
469:
464:
459:
454:
449:
444:
439:
433:
430:
429:
426:
425:
422:
421:
416:
411:
406:
401:
396:
390:
387:
386:
383:
382:
379:
378:
373:
368:
363:
358:
353:
348:
343:
338:
333:
328:
323:
318:
313:
308:
303:
298:
293:
288:
283:
278:
272:
270:and frameworks
266:
265:
262:
261:
258:
257:
252:
247:
242:
237:
232:
227:
221:
218:
217:
214:
213:
210:
209:
204:
199:
194:
189:
184:
179:
174:
169:
164:
158:
155:
154:
151:
150:
144:
143:
135:
134:
49:
47:
40:
26:
24:
14:
13:
10:
9:
6:
4:
3:
2:
1845:
1834:
1831:
1830:
1828:
1813:
1805:
1803:
1795:
1793:
1785:
1784:
1781:
1767:
1764:
1762:
1759:
1757:
1754:
1752:
1749:
1747:
1744:
1742:
1739:
1735:
1732:
1731:
1730:
1727:
1725:
1722:
1720:
1717:
1715:
1712:
1710:
1707:
1705:
1702:
1700:
1697:
1695:
1692:
1691:
1689:
1687:
1683:
1677:
1674:
1672:
1669:
1668:
1666:
1664:
1660:
1654:
1651:
1649:
1646:
1644:
1641:
1640:
1638:
1636:
1632:
1629:
1625:
1619:
1616:
1614:
1611:
1609:
1606:
1604:
1601:
1600:
1598:
1594:
1588:
1585:
1583:
1580:
1578:
1575:
1573:
1572:Incorrectness
1570:
1568:
1565:
1564:
1562:
1558:
1552:
1549:
1545:
1542:
1541:
1540:
1539:Specification
1537:
1535:
1531:
1528:
1526:
1523:
1521:
1518:
1516:
1513:
1511:
1508:
1507:
1505:
1501:
1498:
1496:
1492:
1482:
1479:
1477:
1474:
1472:
1469:
1467:
1464:
1462:
1459:
1455:
1452:
1451:
1450:
1447:
1446:
1444:
1442:
1438:
1432:
1429:
1427:
1424:
1422:
1419:
1417:
1414:
1412:
1409:
1407:
1404:
1402:
1399:
1397:
1394:
1392:
1391:Effect system
1389:
1387:
1384:
1382:
1379:
1375:
1372:
1371:
1370:
1367:
1365:
1362:
1360:
1357:
1356:
1354:
1352:
1348:
1345:
1341:
1331:
1328:
1326:
1325:State machine
1323:
1321:
1318:
1316:
1313:
1311:
1308:
1306:
1303:
1302:
1300:
1298:
1294:
1286:
1283:
1281:
1278:
1277:
1276:
1273:
1269:
1266:
1265:
1264:
1261:
1259:
1256:
1255:
1253:
1249:
1246:
1244:
1240:
1235:
1225:
1222:
1220:
1217:
1215:
1212:
1210:
1207:
1205:
1202:
1200:
1197:
1195:
1192:
1190:
1187:
1185:
1182:
1180:
1177:
1176:
1174:
1170:
1166:
1159:
1154:
1152:
1147:
1145:
1140:
1139:
1136:
1129:
1124:
1120:
1119:
1115:
1109:
1105:
1101:
1096:
1092:
1088:
1084:
1078:
1074:
1070:
1066:
1061:
1054:
1053:
1047:
1046:
1042:
1032:
1029:
1025:
1019:
1016:
1009:
1005:
1002:
1000:
997:
995:
992:
990:
987:
985:
982:
980:
977:
976:
972:
970:
965:
957:
955:
953:
944:
942:
940:
933:
925:
923:
918:
910:
908:
906:
902:
896:
888:
886:
884:
883:effect region
880:
873:
872:Effect system
865:
863:
861:
857:
852:
850:
842:
841:Type checking
839:
838:
837:
833:
825:
823:
818:
810:
808:
806:
805:SQL injection
802:
795:
787:
785:
783:
777:
769:
767:
765:
756:
753:
749:
748:
747:
744:
742:
738:
734:
729:
724:
716:
714:
712:
708:
703:
701:
697:
693:
689:
677:
672:
670:
665:
663:
658:
657:
655:
654:
647:
644:
643:
637:
636:
629:
626:
624:
621:
619:
616:
615:
609:
608:
601:
598:
596:
593:
591:
588:
586:
583:
581:
578:
576:
573:
571:
568:
566:
563:
561:
558:
557:
551:
550:
543:
540:
538:
535:
533:
530:
528:
525:
523:
520:
518:
515:
513:
510:
508:
505:
503:
500:
499:
496:
491:
490:
483:
480:
478:
475:
473:
470:
468:
465:
463:
460:
458:
455:
453:
450:
448:
445:
443:
440:
438:
435:
434:
428:
427:
420:
417:
415:
412:
410:
407:
405:
404:Documentation
402:
400:
397:
395:
392:
391:
385:
384:
377:
374:
372:
369:
367:
364:
362:
359:
357:
354:
352:
349:
347:
344:
342:
339:
337:
334:
332:
329:
327:
324:
322:
319:
317:
314:
312:
309:
307:
304:
302:
299:
297:
294:
292:
289:
287:
284:
282:
279:
277:
274:
273:
269:
268:Methodologies
264:
263:
256:
253:
251:
248:
246:
243:
241:
238:
236:
233:
231:
228:
226:
223:
222:
216:
215:
208:
205:
203:
200:
198:
195:
193:
190:
188:
185:
183:
180:
178:
175:
173:
170:
168:
165:
163:
162:Data modeling
160:
159:
153:
152:
149:
145:
141:
140:
131:
128:
120:
117:February 2018
109:
106:
102:
99:
95:
92:
88:
85:
81:
78: –
77:
73:
72:Find sources:
66:
62:
56:
55:
50:This article
48:
44:
39:
38:
33:
19:
1734:Isabelle/HOL
1551:Verification
1534:completeness
1426:Type systems
1369:Control flow
1263:Denotational
1204:Polyvariance
1172:Key concepts
1164:
1103:
1064:
1051:
1031:
1018:
989:Polyvariance
967:
948:
935:
920:
900:
898:
882:
878:
875:
860:boxed arrays
853:
846:
835:
826:Type systems
820:
797:
779:
770:Control-flow
761:
745:
730:
726:
704:
691:
685:
522:UML Modeling
517:GUI designer
182:Construction
172:Requirements
123:
114:
104:
97:
90:
83:
71:
59:Please help
54:verification
51:
1663:Lightweight
1525:Side effect
1421:Termination
1275:Operational
1184:Correctness
1026:. Springer.
879:effect kind
849:interpreter
832:Type system
733:undecidable
240:Prototyping
235:Incremental
207:Maintenance
187:Engineering
1618:Union-find
1582:Separation
1520:Refinement
1386:Dependence
1285:Small-step
1194:Invariants
1010:References
945:Monitoring
612:Glossaries
202:Deployment
87:newspapers
1714:HOL Light
1544:Languages
1530:Soundness
1449:Data-flow
1431:Typestate
1381:Data-flow
1310:Petri net
1258:Axiomatic
1243:Semantics
431:Practices
255:Waterfall
230:Cleanroom
197:Debugging
167:Processes
1827:Category
1812:Glossary
1792:Category
1729:Isabelle
1613:Hashcons
1587:Temporal
1503:Concepts
1343:Analyses
1280:Big-step
1091:10551500
973:See also
856:inferred
640:Outlines
570:ISO 9001
512:Profiler
507:Debugger
502:Compiler
477:Stand-up
1802:Outline
1608:E-graph
1481:Testing
1466:Fuzzing
1441:Dynamic
1406:Pointer
926:Testing
311:Lean SD
250:V model
192:Testing
101:scholar
1577:Linear
1560:Logics
1396:Escape
1351:Static
1297:Models
1089:
1079:
585:SWEBOK
306:Kanban
281:DevOps
245:Spiral
177:Design
103:
96:
89:
82:
74:
1766:Twelf
1756:NuPRL
1751:Mizar
1724:Idris
1671:Alloy
1627:Tools
1567:Hoare
1411:Shape
1364:Alias
1251:Types
1087:S2CID
1056:(PDF)
901:model
580:PMBOK
495:Tools
356:SEMAT
351:Scrum
225:Agile
108:JSTOR
94:books
1746:LEGO
1741:Lean
1719:HOL4
1699:Agda
1694:ACL2
1676:TLA+
1532:and
1374:kCFA
1077:ISBN
881:and
698:and
595:IREB
590:ITIL
560:CMMI
437:ATDD
346:SAFe
316:LeSS
291:DSDM
80:news
1761:PVS
1704:Coq
1653:SMT
1648:SAT
1643:CHC
1603:BDD
1069:doi
686:In
600:OMG
527:IDE
482:TDD
472:SBE
462:DDD
447:CCO
442:BDD
366:TSP
361:TDD
341:RUP
336:RAD
331:PSP
326:MSF
321:MDD
301:IID
296:FDD
286:DAD
276:ASD
63:by
1829::
1709:F*
1106:.
1085:.
1075:.
954:.
690:,
467:PP
457:CD
452:CI
376:XP
371:UP
1157:e
1150:t
1143:v
1110:.
1093:.
1071::
1058:.
764:C
675:e
668:t
661:v
130:)
124:(
119:)
115:(
105:·
98:·
91:·
84:·
57:.
34:.
20:)
Text is available under the Creative Commons Attribution-ShareAlike License. Additional terms may apply.
